Formal Verification of Software

Code:

CC4008

Acronym:

CC4008

Level:

400

Keywords
Classification	Keyword
OFICIAL	Computer Science

Instance: 2015/2016 - 2S

Active?	Yes
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	13	Study plan since 2014/2015	1	-	6	42	162
MI:ERS	15	Plano Oficial desde ano letivo 2014	4	-	6	42	162

Teaching language

English

Objectives

To understand current trends in Program Verification techniques and approaches, to the certification of program properties, namely model checking and deductive methods.

Learning outcomes and competences

Students should:

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

-to be able to model simple computer systems and to specify properties using temporal logics;

-to annotate programs to ensure safety and functional properties;

Working method

Presencial

Program

- Model checking of reactive systems

Reactive systems; temporal lógics: linear (LTL) and branching (CTL); model checkers (NUSMV); Symbolic model checking: BDDs and OBDDs

Automata based model checking algorithms.

- Program verification

Partial and total correctness calculus (Hoare logics). Verification condition generators. Tools for the specification , verification and certification of imperativ programs

Mandatory literature

Huth Michael 1962-; Logic in Computer Science. ISBN: 0-521-54310-X
Almeida José Bacelar 070; Rigorous software development. ISBN: 9780857290175

Complementary Bibliography

Baier Christel; Principles of model checking. ISBN: 978-0-262-02649-9
Bérard Béatrice 070; Systems and software verification. ISBN: 9783540415237

Teaching methods and learning activities

Lectures and case studies.

Evaluation Type

Distributed evaluation with final exam

Assessment Components

designation	Weight (%)
Exame	50,00
Teste	50,00
Total:	100,00

Amount of time allocated to each course unit

designation	Time (hours)
Estudo autónomo	50,00
Frequência das aulas	50,00
Total:	100,00

Calculation formula of final grade

The final grade is the arithmetic mean of the classifications obtained in a first test, to be in the middle of the semester, and in a second test, in the normal examination period.