You need to activate javascript for this site.
Menu Conteúdo Rodapé
  1. Home
  2. Courses
  3. Computer Science and Engineering
  4. Program Verification and Semantics

Program Verification and Semantics

Code 11480
Year 1
Semester S2
ECTS Credits 6
Workload PL(30H)/T(30H)
Scientific area Informatics
Mode of delivery face-to-face
Learning outcomes Mastering the life cycle of the formal software development.
Apply Formal Methods Specification and verification of software development Upon completion of the UC, students should

- Know how to build and formally specify a system, prove the correctness of the latter and
- Be prepared to address the stages of rapid prototyping and production implementations proven to be reliable
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.
Planned learning activities and teaching methods
The assessment is done by a written exam and continuous assessment based on practical exercises delivered to the teaching staff.
Language Portuguese. Tutorial support is available in English.
Last updated on: 2016-11-16

The cookies used in this website do not collect personal information that helps to identify you. By continuing you agree to the cookie policy.