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.

2022W, VU, 2.0h, 3.0EC, wird geblockt abgehalten
TUWEL

Merkmale

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

Lernergebnisse

Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage

  • Systeme formal zu beschreiben und deren Korrektheit zu spezifizieren (Transitionsrelationen, Automaten, Temporallogik).
  • Moderne Model Checking Algorithmen und Werkzeuge zu verstehen und einzusetzen.
  • Entscheidungsprozeduren (für Erfüllbarkeit) zu verstehen und für die Entwicklung von Model Checking Tools einzusetzen.

 

 

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.

Methoden

The course is composed of 6 (blocked) lectures, which will take place online via Zoom.

Prüfungsmodus

Schriftlich

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

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Fr.12:00 - 15:0011.11.2022 - 13.01.2023 https://tuwien.zoom.us/j/98614265444?pwd=Rzkyd0haZU1XUzlDN2NvRFpRa3I0Zz09 (LIVE)Online Lecture
Computer Aided Verification - Einzeltermine
TagDatumZeitOrtBeschreibung
Fr.11.11.202212:00 - 15:00 https://tuwien.zoom.us/j/98614265444?pwd=Rzkyd0haZU1XUzlDN2NvRFpRa3I0Zz09Online Lecture
Fr.18.11.202212:00 - 15:00 https://tuwien.zoom.us/j/98614265444?pwd=Rzkyd0haZU1XUzlDN2NvRFpRa3I0Zz09Online Lecture
Fr.25.11.202212:00 - 15:00 https://tuwien.zoom.us/j/98614265444?pwd=Rzkyd0haZU1XUzlDN2NvRFpRa3I0Zz09Online Lecture
Fr.02.12.202212:00 - 15:00 https://tuwien.zoom.us/j/98614265444?pwd=Rzkyd0haZU1XUzlDN2NvRFpRa3I0Zz09Online Lecture
Fr.09.12.202212:00 - 15:00 https://tuwien.zoom.us/j/98614265444?pwd=Rzkyd0haZU1XUzlDN2NvRFpRa3I0Zz09Online Lecture
Fr.16.12.202212:00 - 15:00 https://tuwien.zoom.us/j/98614265444?pwd=Rzkyd0haZU1XUzlDN2NvRFpRa3I0Zz09Online Lecture
Fr.13.01.202312:00 - 15:00 https://tuwien.zoom.us/j/98614265444?pwd=Rzkyd0haZU1XUzlDN2NvRFpRa3I0Zz09Online Lecture
LVA wird geblockt abgehalten

Leistungsnachweis

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.

LVA-Anmeldung

Von Bis Abmeldung bis
28.10.2022 00:00 13.01.2023 00:00 13.01.2023 00:00

Curricula

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Vorkenntnisse

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

Sprache

Englisch