Certified verification of relational properties

DOI10.1007/978-3-031-07727-2_6zbMath1502.68077arXiv2202.10349OpenAlexW4285160958MaRDI QIDQ2165505

Lionel Blatter, Virgile Prevosto, Nikolai Kosmatov, Pascale Le Gall

Publication date: 19 August 2022

Full work available at URL: https://arxiv.org/abs/2202.10349

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Constraint-based relational verification
• Verification of sequential and concurrent programs
• Formal verification of a C-like memory model and its uses for verifying program transformations
• Relational program reasoning using compiler IR
• Modular product programs
• Secure information flow by self-composition
• Simple relational correctness proofs for static analyses and program transformations
• Iris from the ground up: A modular foundation for higher-order concurrent separation logic
• Towards Modularly Comparing Programs Using Automated Theorem Provers
• Avoiding exponential explosion
• An axiomatic basis for computer programming
• Property directed self composition

This page was built for publication: Certified verification of relational properties