181.145 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.

2024S, VU, 2.0h, 3.0EC, to be held in blocked form

Course evaluation


  • Semester hours: 2.0
  • Credits: 3.0
  • Type: VU Lecture and Exercise
  • Format: Presence

Learning outcomes

After successful completion of the course, students are able to 

  • Specify correctness of a system: assertions, automata, temporal logic.
  • Understand algorithms for verification of systems: model checking and abstract interpretation.
  • Use constraint solvers (satisfiability solvers) for building  model checkers

Subject of course

Modeling of hardware and software, overview of computer aided verification methods. Specification by temporal logic and automata, state explosion, explicit model checking, symbolic model checking with BDDs, bounded model checking with SAT, abstraction. Modeling and specification languages (Promela, SMV). Verification software in practice (Spin, NuSMV), overview of verification methods for specific classes of systems and current developments.

Teaching methods

The course is composed of 8 lectures and 4 exercises sessions, in which students present examples from exercise sheets.


Mode of examination


Additional information

Registration about TISS Students of Studies 931, 938 are prefered. Please, subscribe the lecture.

ECTS Breakdown:
25h lectures and examination
35h preparation for examination
15h exercises
75h (3 ECTS)



Course dates

Wed13:00 - 15:0013.03.2024 - 12.06.2024Seminarraum FAV 01 B (Seminarraum 187/2) Lecture
Computer Aided Verification - Single appointments
Wed13.03.202413:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Lecture
Wed20.03.202413:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Lecture
Wed10.04.202413:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Lecture
Wed17.04.202413:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Lecture
Wed24.04.202413:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Lecture
Wed08.05.202413:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Lecture
Wed15.05.202413:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Lecture
Wed22.05.202413:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Lecture
Wed29.05.202413:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Lecture
Wed05.06.202413:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Lecture
Wed12.06.202413:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Lecture
Course is held blocked

Examination modalities

The course will have a final exam. The date of the final written exam will be announced later. Students are allowed to bring one A4-size sheet of hand-written notes to the exam. No other material is allowed.



DayTimeDateRoomMode of examinationApplication timeApplication modeExam
Wed13:00 - 15:0026.06.2024EI 4 Reithoffer HS written15.05.2024 08:00 - 24.06.2024 23:55TISSComputer Aided Verification

Course registration

Begin End Deregistration end
07.03.2024 12:00 06.06.2024 12:00 06.07.2024 12:00

Registration modalities

aktuelle Infos bitte LVA abonnieren Ort: TISS



No lecture notes are available.

Previous knowledge

Bachelor in Computer Science/Informatics or related fields. It is recommended to attend this course after Formal Methods in Computer Science (185.291), as topics such as temporal logics are covered in less detail in the CAV lectures.

Accompanying courses


  • Attendance Required!