Extracting program logics from abstract interpretations defined by logical relations

DOI10.1016/J.ENTCS.2007.02.042MaRDI QIDQ5262946zbMATH OpenOpenAlexFDO

Authors 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

abstract interpretationGalois connectionlogical relationtemporal logic

Mathematics Subject Classification ID

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

Recommendations

• Internal and External Logics of Abstract Interpretations
• Safety of abstract interpretations for free, via logical relations and Galois connections
• Abstract Interpretation, Logical Relations, and Kan Extensions
• Logical approximation for program analysis
• Abstract interpretation and application to logic programs

Cites work

• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
• A calculus of logical relations for over- and underapproximating static analyses
• Abstract Interpretation Frameworks
• Abstract Interpretation, Logical Relations, and Kan Extensions
• Algebraic laws for nondeterminism and concurrency
• Comparing Completeness Properties of Static Analyses and Their Logics
• Compiler optimization correctness by temporal logic
• Concrete domains
• Domain theory in logical form
• Generating data flow analysis algorithms from modal specifications
• scientific article; zbMATH DE number 3938547 (Why is no real title available?)
• scientific article; zbMATH DE number 3735770 (Why is no real title available?)
• scientific article; zbMATH DE number 3635472 (Why is no real title available?)
• scientific article; zbMATH DE number 1324833 (Why is no real title available?)
• scientific article; zbMATH DE number 1936671 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• scientific article; zbMATH DE number 1834576 (Why is no real title available?)
• scientific article; zbMATH DE number 2090019 (Why is no real title available?)
• scientific article; zbMATH DE number 821282 (Why is no real title available?)
• scientific article; zbMATH DE number 898449 (Why is no real title available?)
• Making abstract interpretations complete
• On powerdomains and modality
• Pair algebra and its application to automata theory
• Programming Languages and Systems
• Property preserving abstractions for the verification of concurrent systems
• Static Analysis
• Temporal abstract interpretation
• The octagon abstract domain
• The structure of Galois connections
• Two-level semantics and abstract interpretation
• Underapproximating Predicate Transformers
• Verification, Model Checking, and Abstract Interpretation

Cited in

(4)

• Safety of abstract interpretations for free, via logical relations and Galois connections
• Controlling Program Extraction in Light Logics
• scientific article; zbMATH DE number 1953281 (Why is no real title available?)
• Internal and External Logics of Abstract Interpretations

Describes a project that uses

Uses Software

• Octagon

This page was built for publication: Extracting program logics from abstract interpretations defined by logical relations

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