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.

Anmeldung über TISS Studierende der Kennzahlen 931,938 werden bevorzugt. Weitere Informationen finden sich auf TUWEL.

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