Search for contacts, projects,
courses and publications

Computer Aided Verification

Description

This course introduces the students to an approach to validation of hardware and software based on formal analysis of system behaviors. Among the formal methods, model checking enjoys considerable popularity because of its relatively high degree of automation. This approach has been highly effective in the analysis of CPS. The course presents the foundations of model checking starting from the modelling of systems and properties, and then proceeding with the basic algorithms for model checking. Among other things, the distinction between branching time and linear time is discussed, safety and liveness properties are defined, and the use of logics and automata as specifications is discussed. Various logics are introduced, including CTL*, CTL, and LTL. It is shown that model checking for CTL can be reduced to the computation of fixed points of appropriate monotonic functions, and that LTL model checking is based on the translation of the given formula into a Buechi automaton.

 

 

REFERENCES

  • Technical papers and reference manuals related to case studies provided by the Professor.

People

 

Sharygina N.

Course director

Marescotti M.

Assistant

Additional information

Semester
Spring
Academic year
2018-2019
ECTS
6
Language
English
Education
Master of Science in Financial Technology and Computing, Elective course, Lecture, 2nd year

Master of Science in Informatics, Elective course, Lecture, 1st year

Master of Science in Informatics, Elective course, Lecture, 2nd year

PhD programme of the Faculty of Informatics, Elective course, Lecture, 1st year (4 ECTS)

PhD programme of the Faculty of Informatics, Elective course, Lecture, 2nd year (4 ECTS)