Syntactic and semantic soundness of structural dataflow analysis

DOI10.1007/978-3-030-32304-2_6MaRDI QIDQ6536282zbMATH OpenFDO

Authors Patrick Cousot

Publication date 19 April 2024

Full work available at URL https://doi.org/10.1007/978-3-030-32304-2_6

zbMATH Keywords

model checkingabstract interpretationsoundnessdataflow analysis

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 3938555
• Data flow analysis as model checking
• Decidability of the analysis problem for dataflow models of programs
• Bottom-up dataflow analysis of normal logic programs
• On the complexity of flow-sensitive dataflow analyses

Cites work

• scientific article; zbMATH DE number 3463168 (Why is no real title available?)
• scientific article; zbMATH DE number 3485178 (Why is no real title available?)
• scientific article; zbMATH DE number 3557197 (Why is no real title available?)
• scientific article; zbMATH DE number 1927580 (Why is no real title available?)
• scientific article; zbMATH DE number 3402095 (Why is no real title available?)
• A Comparison of Two Algorithms for Global Data Flow Analysis
• A lattice-theoretical fixpoint theorem and its applications
• A program data flow analysis procedure
• Abstract semantic dependency
• Bi-inductive structural semantics
• Combining model checking and data-flow analysis
• Constructive design of a hierarchy of semantics of a transition system by abstract interpretation
• Constructive versions of Tarski's fixed point theorems
• Data flow analysis as model checking
• Generating data flow analysis algorithms from modal specifications
• Making abstract interpretations complete
• Structural analysis: A new approach to flow analysis in optimizing compilers
• Systematic design of program transformation frameworks by abstract interpretation
• Temporal abstract interpretation
• The powerset operator on abstract interpretations

Cited in

(2)

• Coinductive streams in monoidal categories
• Abstract semantic dependency

This page was built for publication: Syntactic and semantic soundness of structural dataflow analysis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6536282)