Relational decomposition

DOI10.1007/978-3-642-22863-6_6MaRDI QIDQ3087994zbMATH OpenOpenAlexFDO

Authors 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

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Recommendations

• Relational logic with framing and hypotheses
• Relational separation logic
• Publication:3204444
• Product programs and relational program logics
• A machine-checked framework for relational separation logic

Cites work

• scientific article; zbMATH DE number 46957 (Why is no real title available?)
• scientific article; zbMATH DE number 1948157 (Why is no real title available?)
• A formally verified compiler back-end
• A logic for information flow in object-oriented programs
• A program logic for resources
• Automated soundness proofs for dataflow analyses and transformations via local rules
• Automatic numeric abstractions for heap-manipulating programs
• Beyond 2-safety: asymmetric product programs for relational program verification
• Generating compiler optimizations from proofs
• Inter-program Properties
• On flow-sensitive security types
• Power simulation and its relation to traces and failures refinement
• Precise and automated contract-based reasoning for verification and certification of information flow properties of programs with arrays
• Prespecification in data refinement
• Program and proof optimizations with type systems
• Relational decomposition
• Relational separation logic
• Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
• Simple relational correctness proofs for static analyses and program transformations
• Stack-based access control and secure information flow
• Static Analysis
• The weakest prespecification
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Verified software toolchain (invited talk)

Cited in

(19)

• Decomposably linear relations
• Decomposing a relation into a tree of binary relations
• scientific article; zbMATH DE number 3902086 (Why is no real title available?)
• Relational decomposition through partial functional dependencies
• Abstraction and subsumption in modular verification of C programs
• Modular verification of procedure equivalence in the presence of memory allocation
• Product programs and relational program logics
• scientific article; zbMATH DE number 3907810 (Why is no real title available?)
• Decomposition of k-ary relations
• Relational verification via invariant-guided synchronization
• Alignment complete relational Hoare logics for some and all
• scientific article; zbMATH DE number 887768 (Why is no real title available?)
• scientific article; zbMATH DE number 723839 (Why is no real title available?)
• Relational decomposition
• Abstraction and subsumption in modular verification of C programs
• Deciding absorption in relational structures
• MORE RESULTS ON DECOMPOSITION AND DECOUPLING OF SINGLE RELATION SYSTEMS
• Relational program reasoning using compiler IR
• Relational logic with framing and hypotheses

Describes a project that uses

Uses Software

• Toolchain
• SPARK

This page was built for publication: Relational decomposition

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