Search for contacts, projects,
courses and publications

Computer Aided Verification

Description

This course covers fundamental algorithms and modeling techniques for formal verification of computer systems. In particular, it covers topics such as model checking, satisfiability (SAT) solving and satisfiability modulo theories (SMT). These techniques have become essential tools for the design and analysis of both hardware designs and software systems. These methods allow the designer exhaustively check if a system satisfies its specification, or to systematically seek for cases where it fails to do so. The emphasis is on the underlying logical and automata-theoretic concepts, the algorithmic solutions, and heuristics to cope with the high computational complexity. Students will experiment with checking the system correctness by writing formal proofs manually and by applying fully automated verification tools.

The course will not be offered in the academic year 2016/17

REFERENCES

  • Validation of Evolving Software; Editors: Chockler, H., Kroening, D., Mariani, L., Sharygina, N. (Eds.); 2015; Springer International Publishing (ISBN 978-3-319-10623-6) 

People

 

Sharygina N.

Course director

Asadi S.

Assistant

Additional information

Semester
Spring
Academic year
2016-2017
ECTS
6
Education
Master of Science in Informatics, Core course, Lecture, 1st and 2nd year

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