Syntactic and Semantic Soundness of Structural Dataflow Analysis

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We show that the classical approach to the soundness of dataflow analysis is with respect to a syntactic path abstraction that may be problematic with respect to a semantics trace-based specification. The fix is a rigorous abstract interpretation based approach to formally construct dataflow analysis algorithms by calculational design.

Original languageEnglish (US)
Title of host publicationStatic Analysis - 26th International Symposium, SAS 2019, Proceedings
EditorsBor-Yuh Evan Chang
PublisherSpringer
Pages96-117
Number of pages22
ISBN (Print)9783030323035
DOIs
StatePublished - Jan 1 2019
Event26th International Static Analysis Symposium, SAS 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019 - Porto, Portugal
Duration: Oct 8 2019Oct 11 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11822 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference26th International Static Analysis Symposium, SAS 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019
CountryPortugal
CityPorto
Period10/8/1910/11/19

    Fingerprint

Keywords

  • Abstract interpretation
  • Dataflow analysis
  • Model-checking
  • Soundness

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Cousot, P. (2019). Syntactic and Semantic Soundness of Structural Dataflow Analysis. In B-Y. E. Chang (Ed.), Static Analysis - 26th International Symposium, SAS 2019, Proceedings (pp. 96-117). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11822 LNCS). Springer. https://doi.org/10.1007/978-3-030-32304-2_6