@inproceedings{acfdb371a872417fb36bfe41c6d7757f,
title = "Syntactic and Semantic Soundness of Structural Dataflow Analysis",
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.",
keywords = "Abstract interpretation, Dataflow analysis, Model-checking, Soundness",
author = "Patrick Cousot",
note = "Funding Information: Let us leave the conclusion to an anonymous reviewer. “It is an old story that the dataflow analysis framework (”syntactic” dataflow analysis in paper{\textquoteright}s characterization) is way too weak. For modern programming languages, control flow is not syntactic but a part of semantics. Dataflow analysis assumes the control flow to be available before the analysis hence a stalemate for modern languages with higher order functions, dynamic bindings, or dynamic gotos; dataflow analysis has neither a systematic guide to prove the correctness of an analysis nor systematic approach to manage the precision of the analysis. On the other hand, the semantics-based design theory (abstract interpretation) is general enough to handle any kind of source languages and powerful enough to prove the correctness and to manage its precision.” Acknowledgement. I thank Sandrine Blazy, Xavier Leroy, and Francesco Ran-zato for lively discussions. I thank the reviewers for their livable comments. This work was supported in part by NSF Grant CNS-1446511. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the National Science Foundation.; 26th International Static Analysis Symposium, SAS 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019 ; Conference date: 08-10-2019 Through 11-10-2019",
year = "2019",
doi = "10.1007/978-3-030-32304-2_6",
language = "English (US)",
isbn = "9783030323035",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "96--117",
editor = "Chang, {Bor-Yuh Evan}",
booktitle = "Static Analysis - 26th International Symposium, SAS 2019, Proceedings",
}