181.145 Computer Aided Verification
Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.
Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.

2021S, VU, 2.0h, 3.0EC, wird geblockt abgehalten


  • Semesterwochenstunden: 2.0
  • ECTS: 3.0
  • Typ: VU Vorlesung mit Übung
  • Format der Abhaltung: Distance Learning


Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage...

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



Inhalt der Lehrveranstaltung

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.


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

The lectures and exercise sessions will take place online via Zoom.



Weitere Informationen

Anmeldung über TISS Studierende der Kennzahlen 931,938 werden bevorzugt. Bitte LVA abonnieren.

ECTS Breakdown:
25h Vorlesungen und Prüfung
35h Prüfungsvorbereitung
15h Übungsaufgaben
75h (3 ECTS)

Vortragende Personen


LVA Termine

Di.15:00 - 16:3023.03.2021 - 18.05.2021 (LIVE)CAV Vorlesung
Do.15:00 - 16:3025.03.2021 - 27.05.2021 CAV Vorlesung
Computer Aided Verification - Einzeltermine
Di.23.03.202115:00 - 16:30 CAV Vorlesung
Do.25.03.202115:00 - 16:30 CAV Vorlesung
Di.13.04.202115:00 - 16:30 CAV Vorlesung
Do.15.04.202115:00 - 16:30 CAV Vorlesung
Di.20.04.202115:00 - 16:30 CAV Vorlesung
Do.22.04.202115:00 - 16:30 CAV Vorlesung
Di.27.04.202115:00 - 16:30 CAV Vorlesung
Do.29.04.202115:00 - 16:30 CAV Vorlesung
Di.04.05.202115:00 - 16:30 CAV Vorlesung
Do.06.05.202115:00 - 16:30 CAV Vorlesung
Di.11.05.202115:00 - 16:30 CAV Vorlesung
Di.18.05.202115:00 - 16:30 CAV Vorlesung
Do.20.05.202115:00 - 16:30 CAV Vorlesung
Do.27.05.202115:00 - 16:30 CAV Vorlesung
LVA wird geblockt abgehalten


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.

Examination form: Online written exam via TUWEL. During the exam, the examiners and the students are connected via audio and video in a online meeting. Solutions are scanned and uploaded by the student within the time specified by the examiner (approx. 5 minutes).


Von Bis Abmeldung bis
04.03.2021 12:00 03.06.2021 12:00 03.07.2021 12:00


aktuelle Infos bitte LVA abonnieren Ort: TISS



Es wird kein Skriptum zur Lehrveranstaltung angeboten.


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.

Begleitende Lehrveranstaltungen

Weitere Informationen

  • Anwesenheitspflicht!