Verification of Programs

Code:

CC4085

Acronym:

CC4085

Level:

400

Keywords
Classification	Keyword
OFICIAL	Computer Science

Instance: 2022/2023 - 2S

Active?	Yes
Web Page:	https://www.dcc.fc.up.pt/~nam/Teaching/vp23/index.php
Responsible unit:	Department of Computer Science
Course/CS Responsible:	Master in Computer Science

Cycles of Study/Courses

Acronym	No. of Students	Study Plan	Curricular Years	Credits UCN	Credits ECTS	Contact hours	Total Time
M:CC	5	Study plan since 2014/2015	1	-	6	42	162

Teaching language

Suitable for English-speaking students

Objectives

In the development of software or hardware computer systems it is essential to ensure their correction in relation to formal specifications.
This course aims to introduce to formal methods using deductive systems  for ertification of program properties.

Learning outcomes and competences

Students should:

• realize the importance of using logic and formal systems in the development of complex it systems;
• be able to annotate simple programs in an imperative or object-oriented language to ensure safety properties and functional properties; and to specify theories that allow the modeling of more complex structures, the correction of which will be demonstrated by an automatic or interactive theorem prover;
• acquire basic concepts of automatic solvers  (SMT-solvers) and interactive theorem provers
• acquire the basic principles in order to allow  to use the appropriate (formal) verification tools in  future working life or the development of research in the field of formal methods;

 

Working method

Presencial

Pre-requirements (prior knowledge) and co-requirements (common knowledge)

Notions of propositional and first-order Logic. Notions of operational semântics and basic algorithms and data structures

Program

 

Axiomatic semantics. Partial and total correctness calculus (Hoare logics). Verification condition generators. Tools for the specification , verification and certification programs. Proposition satisfiability problem (SAT). Satisfiability modulo theories (SMT). Program verification based on dependent types.

Mandatory literature

Almeida José Bacelar 070; Rigorous software development. ISBN: 9780857290175
Daniel Kroening; Decision procedures. ISBN: 978-3-540-74104-6

Complementary Bibliography

Huth Michael 1962-; Logic in Computer Science. ISBN: 0-521-54310-X
Yves Bertot; Interactive theorem proving and program development. ISBN: 9783540208549 hbk
Benjamim Pierce et al.; Software Foundations (https://softwarefoundations.cis.upenn.edu)

Teaching methods and learning activities

Lectures and case studies.

Software

LEAN
Z3
Coq
Dafny

Evaluation Type

Distributed evaluation with final exam

Assessment Components

designation	Weight (%)
Exame	40,00
Trabalho escrito	30,00
Trabalho prático ou de projeto	30,00
Total:	100,00

Amount of time allocated to each course unit

designation	Time (hours)
Estudo autónomo	80,00
Frequência das aulas	42,00
Trabalho escrito	40,00
Total:	162,00

Eligibility for exams

Attendance a 3/4 of the lectures

Calculation formula of final grade

The final grade is the arithmetic mean of the classifications obtained in practical projects and the exam: 0.6*TP+0.4*E.
Exam has a minimum grade of 6/20 and eche project a minimum grade of 5/20.

Total minimum grade: 9.5 over 20

Classification improvement

Exam for 20