| Topic |
|---|
| Dafny, [Koenig, Leino 2012] |
| PCC: Proof-Carrying Code |
| FM & UML: OCL |
| KeY |
| Z Case Study/Studies |
| Event-B 1 |
| Event-B 2 |
| The model checker NuSMV 2 |
| Spin |
| Uppaal |
| (Other model checkers) |
| PVS 1 |
| PVS 2 |
| Specification and Verification of Haskell Programs
see also use of Haskell as specification language for the formally verified microkernel seL4 |
| Agda2 |