Verification of Programs

Code:

CC4085

Acronym:

CC4085

Level:

400

Keywords
Classification	Keyword
OFICIAL	Computer Science

Instance: 2021/2022 - 2S

Active?	Yes
Web Page:	https://www.dcc.fc.up.pt/~nam/Teaching/vp22/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	7	Study plan since 2014/2015	1	-	6	42	162

Teaching language

Suitable for English-speaking students

Objectives

To understand current trends in Program Verification techniques and approaches, to the certification of program properties.

Learning outcomes and competences

Students should:

-to understand the importance of logic and formal systems for software engineering;

-to annotate programs to ensure safety and functional properties;

- to use automatic and interactive provers

Working method

Presencial

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.

Evaluation Type

Distributed evaluation with final exam

Assessment Components

designation	Weight (%)
Exame	60,00
Trabalho escrito	20,00
Trabalho prático ou de projeto	20,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

final grade > 9.5

Calculation formula of final grade

The final grade is the arithmetic mean of the classifications obtained in practical projects and the exam: 0.4*TP+06*E.

Minimum grade: 9.5 over 20

Examinations or Special Assignments

Exam has a minimum grade of 6/20

Special assessment (TE, DA, ...)

The final grade is the arithmetic mean of the classifications obtained in practical projects and the exam: 0.4*TP+06*E.

Minimum grade: 9.5 over 20

Classification improvement

Exam for 20

Observations

Notions of propositional and first-order Logic.