|
Syllabus |
Contextual Introduction.
Specification, Model and Analysis of Software: Formal specification, abstract machine state, Hoare logic. type theoretic based specification
Specification and Proof of Software: model checking, automatic/interactive proof.
Specification and Deriving Implementations: Program extraction, refinement
Specification and Transformation: abstract interpretation.
|
|
Main Bibliography |
J.B. Almeida, M.J. Frade, J.S. Pinto, and S. Melo de Sousa. Rigorous Software Development, An Introduction to Program Verification, volume 103 of Undergraduate Topics in Computer Science. Springer-Verlag, first edition, 307 p. 52 illus, 2011.
Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci, and Philippe Schnoebelen. Systems and Software Verification. Model-Checking Techniques and Tools. Springer, 2001.
J. Cooke. Constructing correct software. Formal approaches to computing and information technology. Springer Verlag, 2005.
Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Serie. Springer Verlag, 2004.
J-F. Monin. Understanding Formal Methods. Springer Verlag, 2002. Translation editor M. Hinchey.
R. D. Tennent. Specifying Software. A Hands-On Introduction. Cambridge University Press, 2002.
|