Relational Decomposition

DOI10.1007/978-3-642-22863-6_6zbMath1342.68070OpenAlexW2914544883MaRDI QIDQ3087994

Lennart Beringer

Publication date: 17 August 2011

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22863-6_6

Mathematics Subject Classification ID

Related Items (6)

Product programs and relational program logics ⋮ Abstraction and subsumption in modular verification of C programs ⋮ Relational program reasoning using compiler IR ⋮ Unnamed Item ⋮ Modular Verification of Procedure Equivalence in the Presence of Memory Allocation ⋮ Relational Decomposition

Uses Software

• SPARK
• Toolchain

Cites Work

• Unnamed Item
• Unnamed Item
• Prespecification in data refinement
• Relational separation logic
• Program and proof optimizations with type systems
• The weakest prespecification
• Power simulation and its relation to traces and failures refinement
• A program logic for resources
• A formally verified compiler back-end
• Verified Software Toolchain
• Relational Decomposition
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Inter-program Properties
• Simple relational correctness proofs for static analyses and program transformations
• Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification
• Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays
• Stack-based access control and secure information flow
• Automatic numeric abstractions for heap-manipulating programs
• Generating compiler optimizations from proofs
• Automated soundness proofs for dataflow analyses and transformations via local rules
• Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
• On flow-sensitive security types
• A logic for information flow in object-oriented programs
• Static Analysis

This page was built for publication: Relational Decomposition