Extracting Program Logics From Abstract Interpretations Defined by Logical Relations

DOI10.1016/j.entcs.2007.02.042zbMath1316.68042OpenAlexW2061106041MaRDI QIDQ5262946

David A. Schmidt

Publication date: 10 July 2015

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2007.02.042

zbMATH Keywords

Galois connectiontemporal logicabstract interpretationlogical relation

Mathematics Subject Classification ID

Logic in computer science (03B70) Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Galois correspondences, closure operators (in relation to ordered sets) (06A15)

Uses Software

• Octagon

Cites Work

• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
• The octagon abstract domain
• A calculus of logical relations for over- and underapproximating static analyses
• Two-level semantics and abstract interpretation
• On powerdomains and modality
• Domain theory in logical form
• Concrete domains
• Generating data flow analysis algorithms from modal specifications
• Property preserving abstractions for the verification of concurrent systems
• Compiler optimization correctness by temporal logic
• The structure of Galois connections
• Abstract Interpretation, Logical Relations, and Kan Extensions
• Underapproximating Predicate Transformers
• Algebraic laws for nondeterminism and concurrency
• Temporal abstract interpretation
• Abstract Interpretation Frameworks
• Programming Languages and Systems
• Making abstract interpretations complete
• Comparing Completeness Properties of Static Analyses and Their Logics
• Static Analysis
• Pair algebra and its application to automata theory
• Verification, Model Checking, and Abstract Interpretation
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Extracting Program Logics From Abstract Interpretations Defined by Logical Relations