Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage

• Understand and use constraint solvers, in particular satisifiability solvers.
• Understand SAT based model checking algorithms
• Implement model checking algorithms and test them.

Implementierung eines SAT-basierten Model Checking Algorithmus.

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

The course is held online, all Q&A sessions as well as the final presentations will be done on Zoom. For the final presentation students must have a working camera and be able to share their screen.

Anmeldung über TISS Studierende der Kennzahlen 931,938 werden bevorzugt. Bitte LVA 181.145 abonnieren; dort erscheinen die Termine.

ECTS Breakdown:
----------------------------------
60h Übungen
15h Übungspräsentationen
----------------------------------
75h (3 ECTS)
----------------------------------

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.

aktuelle Infos bitte LVA abonnieren Ort: TISS

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