Certified Programming

In the current framework in which the security of systems assumes a key role, the capacity to produce certified code has become essential: the final product of a software project no longer consists exclusively of executable applications, but must be accompanied by certificates assuring that the applications effectively possess the desired properties, be them functional or security properties. For instance, it may be important that a program accomplishes a given policy that deters it from accessing unauthorized resources. Formal Verification is the activity that tries to establish that a system effectively behaves in accordance to its specification, or that it behaves within a prescribed policy.

On the other hand, the emergence of new application areas like Bioinformatics and Cryptography have emphasized the importance of the study of Algorithms and their properties in Computer Science.

The present CSU30 addresses these crucial matters, and establishes competences at two levels:

• At the fundamental level, a solid base of knowledge is built, which is crucial for tackling sophisticated problems in Computing. This is organized in three fundamental areas of Computer Science: Logic and Semantics of Programming, principles of Programming Languages, and the study of Algorithms and their complexity.
• At the applied level, competences in Formal Verification using tools based on models or logic inference, as well in the use of advanced programming language techniques.

Cientific Coordination

• José Bernardo Barros
• Maria João Frade
• Jorge Sousa Pinto
• João Alexandre Saraiva
• Luís Pinto
• José Espirito Santo

Learning Outcomes

• To understand the basic notions of Type Theory, their implications on the type systems of programming languages and their logical interpretation.
• To express logical properties in assisted proof systems, and to conduct proofs in those systems.
• To describe the main complexity classes and the elementary relationships between them.
• To specify, express, and verify the validity of properties (correctness or other properties) of software systems, with the help of assisted proof tools.
• To apply advanced programming techniques (notably in the functional realm) for solving concrete problems.
• To describe characteristics of problems in diverse application areas and to apply, analyse, compare, and design algorithms in those areas.
• To develop integrated software development and verification projects.

Modules

This CSU30 is organised around 3 thematic modules, and one integrated project and seminar. The thematic modules are:

• Programming Foundations (FP)
  • Programming Logic
  • Complexity
• Software Verification (VS)
• Advanced Programming (AP)

Partners