A calculus of logical relations for over- and underapproximating static analyses

DOI10.1016/J.SCICO.2006.03.008MaRDI QIDQ859954zbMATH OpenOpenAlexFDO

Authors David A. Schmidt

Publication date 22 January 2007

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

Full work available at URL https://doi.org/10.1016/j.scico.2006.03.008

zbMATH Keywords

Galois connectionsabstract interpretationHennessy-Milner logicpowerdomainsunderapproximationstate-transition systems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)

Recommendations

• Static Analysis
• A Galois connection calculus for abstract interpretation
• scientific article; zbMATH DE number 2090019
• Comparing Completeness Properties of Static Analyses and Their Logics
• Safety of abstract interpretations for free, via logical relations and Galois connections

Cited in

(7)

• Limits and difficulties in the design of under-approximation abstract domains
• Abstract Interpretation from a Topological Perspective
• Static Analysis
• Extracting program logics from abstract interpretations defined by logical relations
• Underapproximating Predicate Transformers
• A Galois connection calculus for abstract interpretation
• Loop detection in term rewriting using the eliminating unfoldings

This page was built for publication: A calculus of logical relations for over- and underapproximating static analyses

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