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.

2022W, VU, 2.0h, 3.0EC, to be held in blocked form
TUWEL

Properties

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

Learning outcomes

After successful completion of the course, students are able to

  • Formally describe systems and specify their correctness using transition relations, automata, and temporal logic.
  • Understand state-of-the-art model checking algorithms for verification of systems and use verification tools.
  • Use decision procedures (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 6 (blocked) lectures, which will take place online via Zoom.

Mode of examination

Written

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)
----------------------------------

Lecturers

Institute

Course dates

DayTimeDateLocationDescription
Fri12:00 - 15:0011.11.2022 - 13.01.2023 https://tuwien.zoom.us/j/98614265444?pwd=Rzkyd0haZU1XUzlDN2NvRFpRa3I0Zz09 (LIVE)Online Lecture
Computer Aided Verification - Single appointments
DayDateTimeLocationDescription
Fri11.11.202212:00 - 15:00 https://tuwien.zoom.us/j/98614265444?pwd=Rzkyd0haZU1XUzlDN2NvRFpRa3I0Zz09Online Lecture
Fri18.11.202212:00 - 15:00 https://tuwien.zoom.us/j/98614265444?pwd=Rzkyd0haZU1XUzlDN2NvRFpRa3I0Zz09Online Lecture
Fri25.11.202212:00 - 15:00 https://tuwien.zoom.us/j/98614265444?pwd=Rzkyd0haZU1XUzlDN2NvRFpRa3I0Zz09Online Lecture
Fri02.12.202212:00 - 15:00 https://tuwien.zoom.us/j/98614265444?pwd=Rzkyd0haZU1XUzlDN2NvRFpRa3I0Zz09Online Lecture
Fri09.12.202212:00 - 15:00 https://tuwien.zoom.us/j/98614265444?pwd=Rzkyd0haZU1XUzlDN2NvRFpRa3I0Zz09Online Lecture
Fri16.12.202212:00 - 15:00 https://tuwien.zoom.us/j/98614265444?pwd=Rzkyd0haZU1XUzlDN2NvRFpRa3I0Zz09Online Lecture
Fri13.01.202312:00 - 15:00 https://tuwien.zoom.us/j/98614265444?pwd=Rzkyd0haZU1XUzlDN2NvRFpRa3I0Zz09Online Lecture
Course is held blocked

Examination modalities

The course will have a written exam. The date of the final written exam will be announced later. The exam will be an open-book exam.

Course registration

Begin End Deregistration end
28.10.2022 00:00 13.01.2023 00:00 13.01.2023 00:00

Curricula

Literature

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

Language

English