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.
Note for Constructive Logic
2024-05-08This is a note for my learning of Constructive Logic by Frank Pfenning. Logic is the study of the principles of valid inferences and demonstration, which constitutes an important area in the disciplines of philosophy and mathematics.
1