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. 

Registration about TISS Students of Studies 931, 938 are prefered. Further information can be found in TUWEL.

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