Formal Verification of Software

Code:

CC4008

Acronym:

CC4008

Level:

400

Keywords
Classification	Keyword
OFICIAL	Computer Science

Instance: 2017/2018 - 2S

Active?	Yes
Web Page:	http://www.dcc.fc.up.pt/~nam/web/Teaching/vfs18/index.html
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	4	Study plan since 2014/2015	1	-	6	42	162
MI:ERS	19	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

Modelling of parallel systemsL transition systems and concurrency. Linear time properties. Temporal logics: linear (LTL) and branching (CTL); model checkers; 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

Baier Christel; Principles of model checking. ISBN: 978-0-262-02649-9
Almeida José Bacelar 070; Rigorous software development. ISBN: 9780857290175

Complementary Bibliography

Huth Michael 1962-; Logic in Computer Science. ISBN: 0-521-54310-X
Bérard Béatrice 070; Systems and software verification. ISBN: 9783540415237

Teaching methods and learning activities

Lectures and case studies.

Software

spin

Evaluation Type

Distributed evaluation with final exam

Assessment Components

designation	Weight (%)
Exame	40,00
Teste	40,00
Trabalho laboratorial	20,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 practical project, a first test,  to be in the middle of the semester,   and in a second test, in the normal examination period.

Classification improvement

The second exam values 80% of the grade.