Construção e Verificação de Software

Knowledge

The students consolidate their software construction skills for building trustworthy software, in the broad context of modern software systems.

The CU develops the perspective that verification should be tightly integrated with the software construction process, guided by the use of code analysis tools.

Core techniques for the static analysis of code are covered, namely verification of functional programs, the use of Hoare Logic, and the use of Separation Logic.

Knowledge Application

Use rigorous programming methods and verification techniques to ensure the reliability of software.

Develop, in team work, mid-size projects that require developing the specification and verified implementation of non-trivial algorithms and programs.

Use logical assertions to specify, verifiy, and reason about programs correctness, as well as associated tools (Coq, Why3, CFML).

Specify behavioral specifications (invariants, pre-conditions, and post- conditions) to implement modules and their interfaces.