181.144 Computer-Aided Verification
This course is in all assigned curricula part of the STEOP.
This course is in at least 1 assigned curriculum part of the STEOP.

2023S, UE, 2.0h, 3.0EC, to be held in blocked form


  • Semester hours: 2.0
  • Credits: 3.0
  • Type: UE Exercise
  • Format: Online

Learning outcomes

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.

Subject of course

Implementation of a SAT-based model checking algorithm.

Teaching methods

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


Mode of examination

Written and oral

Additional information

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)



Examination modalities

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.

Course registration

Begin End Deregistration end
18.04.2023 14:00 01.07.2023 23:59 15.07.2023 23:59

Registration modalities

Participation in CAV VU is required.


Study CodeObligationSemesterPrecon.Info
066 504 Master programme Embedded Systems Not specified
066 931 Logic and Computation Mandatory elective
066 937 Software Engineering & Internet Computing Mandatory elective
066 938 Computer Engineering Mandatory elective
066 938 Computer Engineering Mandatory


No lecture notes are available.

Previous knowledge

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

Accompanying courses


  • Attendance Required!