Rigorous Software Development.An Introduction to Program Verification (RSD)
Series: Undergraduate Topics in Computer Science
Almeida, J.B., Frade, M.J., Pinto, J.S., Melo de Sousa, S.
1st Edition., 2011, XIII, 307 p. 52 illus.

Program Proofs. K. Leino 2023

Linguagem de anotações Dafny
- Dafny site
- Github
- Install with VSCODE (or Emacs)

Decision Procedures: an algorithmic point of view (DP)
By Daniel Kroening and Ofer Strichman (2016)

SMT-LIB
SMT-COMP
Z3 : guide
Z3 internals
Z3 tutorial

Logic in Computer Science modelling and reasoning about systems (LICS)
Michael Huth and Mark Ryan

Interactive Theorem Proving and Program Development
Yves Bertot and Pierre Casterán
Springer

Exercises