Generating data flow analysis algorithms from modal specifications

DOI10.1016/0167-6423(93)90003-8MaRDI QIDQ1330457zbMATH OpenOpenAlexFDO

Authors Bernhard Steffen

Publication date 21 July 1994

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0167-6423(93)90003-8

zbMATH Keywords

automatic identification of program pointsbit-vector algorithmsdata flow analysis

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Data flow analysis as model checking
• Describing data flow analysis techniques with Kleene algebra
• Decidability of the analysis problem for dataflow models of programs
• Programming Languages and Systems
• Extracting a data flow analyser in constructive logic
• Automatic synthesis of data-flow analyzers
• Combining model checking and data-flow analysis
• Generating model checkers from algebraic specifications
• Efficient dataflow analysis of logic programs

Cited in

(12)

• Specification languages in algebraic compilers
• Automatic synthesis of data-flow analyzers
• Generative program analysis and beyond: the power of domain-specific languages (invited paper)
• Distributed verification of multi-threaded C++ programs
• Combining model checking and data-flow analysis
• Property-oriented expansion
• Unifying models
• Data flow analysis as model checking
• Extracting program logics from abstract interpretations defined by logical relations
• Generating Specialized Rules and Programs for Demand-Driven Analysis
• Syntactic and semantic soundness of structural dataflow analysis
• Model checking as program verification by abstract interpretation

This page was built for publication: Generating data flow analysis algorithms from modal specifications

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