After successful completion of the course, students are able to.
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. Please, subscribe the lecture 181.145, dates will appear there.
ECTS Breakdown:----------------------------------60h exercises15h 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