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

DOI10.1016/j.scico.2006.03.008zbMath1171.68543OpenAlexW2052286082MaRDI QIDQ859954

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

powerdomainsGalois connectionsabstract interpretationHennessy-Milner logicunderapproximationstate-transition systems

Mathematics Subject Classification ID

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

Related Items

Limits and difficulties in the design of under-approximation abstract domains ⋮ Loop detection in term rewriting using the eliminating unfoldings ⋮ Abstract Interpretation from a Topological Perspective ⋮ Extracting Program Logics From Abstract Interpretations Defined by Logical Relations