Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification

DOI10.1007/978-3-642-35722-0_3zbMath1419.68063OpenAlexW5424990MaRDI QIDQ3455833

Gilles Barthe, César Kunz, Juan Manuel Crespo

Publication date: 11 December 2015

Published in: Logical Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-35722-0_3

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Product programs in the wild: retrofitting program verifiers to check information flow security ⋮ Constraint-based relational verification ⋮ Product programs and relational program logics ⋮ RHLE: modular deductive verification of relational \(\forall \exists\) properties ⋮ Relational program reasoning using compiler IR ⋮ Unnamed Item ⋮ Modular Verification of Procedure Equivalence in the Presence of Memory Allocation ⋮ Relational Decomposition

Uses Software

• TVOC
• EasyCrypt
• CoVaC

Cites Work

• Relational separation logic
• Formal verification of a C-like memory model and its uses for verifying program transformations
• Certificate Translation in Abstract Interpretation