This information sheet indicates how the course will be organized at pandemic code level yellow and green.
If the colour codes change during the academic year to orange or red, modifications are possible, for example to the teaching and evaluation methods.

Specification and verification

Course Code :2001WETFSP
Study domain:Computer Science
Academic year:2020-2021
Semester:1st semester
Contact hours:45
Study load (hours):168
Contract restrictions: No contract restriction
Language of instruction:English
Exam period:exam in the 1st semester
Lecturer(s)Guillermo Alberto Perez

3. Course contents *

An important issue in the development of large software systems is the specification of their desired structural and dynamic properties. To avoid the impreciseness and ambiguities of specifications in natural language, a number of specialized formal languages, based on logic and mathematics, have been developed. Moreover, these languages are supported by algorithms and tools allowing various types of analysis and verification.

The course covers the following main topics:

* Formal verification

* Labelled transition systems as models of systems

* Linear temporal logic

* Computation tree logic

* Symbolic model checking

* Automatic controller synthesis