Specification and verification

Course Code :2001WETFSP
Study domain:Computer Science
Bi-anuall course:Taught in academic years starting in an odd year
Academic year:2019-2020
Semester:1st semester
Contact hours:45
Credits:6
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

* Model checking probabilistic systems