Formal Verification of Software

Code:

CC447

Acronym:

CC447

Keywords
Classification	Keyword
OFICIAL	Computer Science

Instance: 2013/2014 - 2S

Active?	Yes
Responsible unit:	Department of Computer Science
Course/CS Responsible:	Master's Degree in Network and Information Systems Engineering

Cycles of Study/Courses

Acronym	No. of Students	Study Plan	Curricular Years	Credits UCN	Credits ECTS	Contact hours	Total Time
M:CC	7	PE do Mestrado em Ciência de Computadores	1	-	7,5	67	202,5
MI:ERS	20	Plano de Estudos a partir de 2007	4	-	7,5	67	202,5

Teaching language

Portuguese

Objectives

...

Learning outcomes and competences

...

Working method

Presencial

Program

...

Mandatory literature

Michael Huth and Mark Ryan; Logic in Computer Science: Modelling and reasoning about systems. , 2004
Bertot Yves; Interactive theorem proving and program development. ISBN: 9783540208549 hbk

Complementary Bibliography

Christel Baier, Joost-Pieter Katoen, and Kim Guldstrand Larsen; Principles of Model Checking, MIT Press, 2008
Winskel Glynn; The formal semantics of programming languages. ISBN: 978-0-262-23169-5
Benjamin C. Pierce; Software Foundations
José Bacelar Almeida,Jorge Sousa Pinto,Maria João Frade,Simão Melo de Sousa ; Rigorous Software Development: An Introduction to Program Verification, Springer-Verlag, 2011. ISBN: 978-0-85729-017-5

Teaching methods and learning activities

...

Software

http://coq.inria.fr/
http://nusmv.fbk.eu/
http://why.lri.fr/

keywords

Physical sciences > Computer science

Evaluation Type

Distributed evaluation without final exam

Assessment Components

designation	Weight (%)
Exame	60,00
Trabalho laboratorial	40,00
Total:	100,00

Calculation formula of final grade

...