Notes for Relational Hoare Logic
2024-07-23This is a note reading the thesis of Lionel Blatter1, which makes contribution to the relational properties verification in the Frama-C ecosystem, and it is also a good material for learning formal verification.
1