# 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: