This repository contains a Coq formalization and proof of soundness for :
- recursive Hoare triple verification with a verification condition generator on a simple language with procedures and aliasing;
- a method for verifying relational properties using a verification condition generator, without relying on code transformation (such as self-composition) or making additional separation hypotheses in case of aliasing;
This project is developed and tested with Rocq version 9.1.0 and OCaml 5.2.0.
This project require currently a modified version of the semantics package, which is available here
To run the whole proof, run
make
- Loc.v: definition of locations.
- Sigma.v: definition of memory state.
- Proc.v: definition of procedure names.
- Aexp.v: definition of arithmetic expressions.
- Bexp.v: definition of boolean expressions.
- Com.v: definition of commands.
- Sem.v: definition of operation and denotational semantics, and useful properties
- Inliner.v: definintion of inliner for procedures and proof of useful property.
- Sem_Prop.v: Relation between operation and denotational semantics
- Hoare_Triple.v: definintion of Hoare Triples and proof of useful property.
- Total.v: definition of total correctness.
- Vcg.v and Vcg_Opt.v: definition of respectively a naive verification condition genrator and a optimized version and proof of useful property.
- Correct.v: proof that Hoare Triples can be verified using verification condition generator.
- Rela.v: definition of relational properties and proof of useful property.
- Vcg_Rela.v: definition of a verification condition generator for Relational Properties using the verification condition generator define in Vcg.v and proof of useful property.
- Correct_Rela.v: proofs that Relational Properties can be verified using verification condition generator.
- Examples.v: some examples.