News
- Die Abmeldefrist vom Proseminar endet am 22.10.2014.
- Die Vortragstermine sind am 9.2. und 10.2.2015 jeweils ab 9:30 Uhr im I2 Seminarraum
Inhalt
Dieses Proseminar hat als Thema bekannte Algorithmen und Werkzeuge aus dem Gebiet der Verifikation sicherheitskritischer Systeme.
Voraussetzungen
Für diese Veranstaltung sind Grundkenntnisse der Automatentheorie, wie sie in der Vorlesung “Formale Systeme, Automaten und Prozesse” vermittelt werden, erforderlich.
Organisation
- Die Themenvergabe erfolgt in der Einführungsveranstaltung.
- Das Proseminar umfasst eine schriftliche Ausarbeitung und eine Präsentation über das vergebene Thema sowie eine Einführung in das Textsatzsystem LaTeX und eine Präsentationsübung.
- Literatur wird nach der Einführungsveranstaltung mit dem jeweiligen Betreuer abgesprochen.
- Die Vorträge werden gegen Ende des Semesters als Blockseminar gehalten.
Termine
- 01.10.2014 16:00 – 17:30 Uhr Einführungsveranstaltung
- In der Woche vom 13.10. bis zum 17.10.: Bibilotheksführung
- 20.10.2014 Betreuer kontaktieren
- 10.11.2014 Struktur der Ausarbeitung
- 12.11.2014 15:30 Uhr Vortragsübung (I2 Seminarraum)
- 08.12.2014 Ausarbeitung erste komplette Version
- 05.01.2015 Endversion Ausarbeitung
- 19.01.2015 Folien erste komplette Version
- 30.01.2015 Endversion Folien
- 09.02.2015, 10.02.2015 Vorträge (Reihenfolge wird vor Ort bekannt gegeben)
Kontakt
Bei Fragen zu diesem Proseminar wenden Sie sich bitte an Stefan Schupp.
Materialien
|
Titel |
Datei |
|
Einführungsveranstaltung |
Proseminarthemen
Eine Liste der Themen, die dieses Semester angeboten werden (die Betreuer werden nach der Themenvergabe bekanntgegeben):
| Thema | Betreuer | Student |
|---|---|---|
| Binary decision diagrams | Ábrahám | Tobias Winkler |
| Bisimulation | Nellen | Phillip Nolte |
| CVC4 | Corzilius | Marco Dung |
| Deduction / theorem proving | Ábrahám | Kevin Batz |
| Equality logic in SMT | Corzilius | Torben Friedrichs |
| Heap abstraction with Juggrnaut | Kremer | Jonathan Neuschäfer |
| iSAT | Schupp | Not Assigned |
| Modelchecking with MRMC / Prism / Storm | Kremer | Deniz Schmidt |
| Mutual exclusion | Schupp | Jerome Bergmann |
| PLC programming | Nellen | Daniel Habering |
| Probabilistic automata | Kremer | Stefan Brunecker |
| Satisfiability | Ábrahám | Hong An Nguyen |
| Satisfiability Modulo Theories | Corzilius | Benedikt Pago |
| Solving Nonlinear Arithmetic via SAT Modulo Linear Arithmetic | Schupp | Stefanie Koß |
| Spaceset representations for hybrid systems | Schupp | Thomas Milde |
| Temporal logic | Ábrahám | Vinzent Skawran |
| Timed automata | Nellen | Not Assigned |
| Uninterpreted functions in SMT | Corzilius | Vincent Ahlrichs |
| Verifying Coreutils | Kremer | Not Assigned |
| Verifying real-time systems with UPPAAL | Nellen | Benjamin Hirsch |
Vortragsreihenfolge:
- BDDs (Tobias Winkler)
- Bisimulation (Philip Nolte)
- Deduction/Theorem proving (Kevin Batz)
- Probabilistic automata (Stefan Brunecker)
- Modelchecking with MRMC/Prism/Storm (Deniz Schmidt)
- Temporal logic (Vinzent Skawran)
- UPPAAL (Benjamin Hirsch)
- Hybrid systems reachability (Thomas Milde)
- Mutual exclusion (Jerome Bergmann)
- PLC programming (Daniel Habering)
- SAT (Hong An Ngyuen)
- SMT (Benedikt Pago)
- Solving LRA via NRA (Stefanie Koß)
- Equality logic in SMT (Torben Friedrichs)
- Uninterpreted functions in SMT (Vincent Ahlrichs)