TWISC Summer School 2006
Application of Formal Verification to Software Security
Slides
Examples used for the presentation:
- Verification of a simple sorting algorithm in Coq
- Examples of verification in Hoare logic in Coq can be found
here
(GCD, string_copy, etc. in examples.v file)
- A paper on verification of memory management using separation logic in Coq (Coq scripts here)
- A short paper on verification of arithmetic functions in SmartMIPS in Coq (Coq scripts not yet available)
- Verification of a simple client-server application in Spin:
- A paper on verification of an embedded operating system in Spin
- Needham-Schroeder protocol in Spin: