Syntactic and Semantic Soundness of Structural Dataflow Analysis

Patrick Cousot

doi:10.1007/978-3-030-32304-2_6

Syntactic and Semantic Soundness of Structural Dataflow Analysis

Patrick Cousot

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Static Analysis - 26th International Symposium, SAS 2019, Proceedings
Editors	Bor-Yuh Evan Chang
Publisher	Springer
Pages	96-117
Number of pages	22
ISBN (Print)	9783030323035
DOIs	https://doi.org/10.1007/978-3-030-32304-2_6
State	Published - 2019
Event	26th International Static Analysis Symposium, SAS 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019 - Porto, Portugal Duration: Oct 8 2019 → Oct 11 2019

Publication series

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

Conference

Conference	26th International Static Analysis Symposium, SAS 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019
Country	Portugal
City	Porto
Period	10/8/19 → 10/11/19

Keywords

Abstract interpretation
Dataflow analysis
Model-checking
Soundness

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-030-32304-2_6

Fingerprint Dive into the research topics of 'Syntactic and Semantic Soundness of Structural Dataflow Analysis'. Together they form a unique fingerprint.

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

Syntactic and Semantic Soundness of Structural Dataflow Analysis. / Cousot, Patrick.

Static Analysis - 26th International Symposium, SAS 2019, Proceedings. ed. / Bor-Yuh Evan Chang. Springer, 2019. p. 96-117 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11822 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Cousot, P 2019, Syntactic and Semantic Soundness of Structural Dataflow Analysis. in B-YE Chang (ed.), Static Analysis - 26th International Symposium, SAS 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11822 LNCS, Springer, pp. 96-117, 26th International Static Analysis Symposium, SAS 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019, Porto, Portugal, 10/8/19. https://doi.org/10.1007/978-3-030-32304-2_6

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

@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",

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",

note = "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",

}

TY - GEN

T1 - Syntactic and Semantic Soundness of Structural Dataflow Analysis

AU - Cousot, Patrick

PY - 2019

Y1 - 2019

N2 - 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.

AB - 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.

KW - Abstract interpretation

KW - Dataflow analysis

KW - Model-checking

KW - Soundness

UR - http://www.scopus.com/inward/record.url?scp=85075830644&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85075830644&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-32304-2_6

DO - 10.1007/978-3-030-32304-2_6

M3 - Conference contribution

AN - SCOPUS:85075830644

SN - 9783030323035

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 96

EP - 117

BT - Static Analysis - 26th International Symposium, SAS 2019, Proceedings

A2 - Chang, Bor-Yuh Evan

PB - Springer

T2 - 26th International Static Analysis Symposium, SAS 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019

Y2 - 8 October 2019 through 11 October 2019

ER -