After successful completion of the course, students are able to.

• Understand and use constraint solvers, in particular satisifiability solvers.
• Understand SAT based model checking algorithms
• Implement model checking algorithms and test them.

Implementation of a SAT-based model checking algorithm.

The students will work individually on building their own SAT based model checkers. 

The course is held online, all Q&A sessions as well as the final presentations will be done on Zoom. For the final presentation students must have a working camera and be able to share their screen.

Registration about TISS Students of Studies 931, 938 are prefered. Please, subscribe the lecture 181.145, dates will appear there.

ECTS Breakdown:
----------------------------------
60h exercises
15h presentation of exercises
----------------------------------
75h (3 ECTS)
----------------------------------

The students are evaluated individually according to the following criteria: suitability of chosen approach, comprehensiveness and precision of project documentation and presentation, quality of results.

Participation in CAV VU is required.

Basic programming skills, no previous experience with verification tools is required