Extracting Program Logics From Abstract Interpretations Defined by Logical Relations

DOI10.1016/J.ENTCS.2007.02.042zbMATH Open1316.68042OpenAlexW2061106041MaRDI QIDQ5262946FDOQ5262946

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 interpretationlogical relationGalois connectiontemporal logic

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (3)

• Safety of abstract interpretations for free, via logical relations and Galois connections
• Title not available (Why is that?)
• Controlling Program Extraction in Light Logics

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)