Extracting program logics from abstract interpretations defined by logical relations
DOI10.1016/J.ENTCS.2007.02.042zbMATH Open1316.68042OpenAlexW2061106041MaRDI QIDQ5262946FDOQ5262946
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
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
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 (4)
Uses Software
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)
