Product programs and relational program logics

DOI10.1016/j.jlamp.2016.05.004zbMath1355.68047OpenAlexW2472147697MaRDI QIDQ2374302

Gilles Barthe, César Kunz, Juan Manuel Crespo

Publication date: 15 December 2016

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2016.05.004

Mathematics Subject Classification ID

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

Related Items

Operationally-based program equivalence proofs using LCTRSs ⋮ Unnamed Item ⋮ Modular Verification of Procedure Equivalence in the Presence of Memory Allocation ⋮ System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory ⋮ Stratified guarded first-order transition systems

Uses Software

• TVOC
• PrivateLR
• SymDiff
• CoVaC

Cites Work

• Relational separation logic
• A semantic approach to secure information flow
• Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy
• Abstract Semantic Differencing for Numerical Programs
• Probabilistic relational reasoning for differential privacy
• Relational Decomposition
• Secure information flow by self-composition
• Simple relational correctness proofs for static analyses and program transformations
• Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification
• An Axiomatic Approach to Information Flow in Programs
• Continuity analysis of programs
• Formal certification of code-based cryptographic proofs
• A logic for information flow in object-oriented programs
• Probabilistic relational verification for cryptographic implementations
• Computer Aided Verification
• Static Analysis
• Differential Privacy