Wintersemester 2021/22
Anwendung Formaler Verifikation
Von der Theorie zur Anwendung
| Veranstaltungstyp: | Seminar |
|---|---|
| Zielgruppe: | Master Informatik |
| Umfang: | 2 SWS / 3 ECTS |
| Termine: |
Kurzvorträge: 2.12.2021 16:00, Raum 236 Hauptvorträge: 3.2.2022 16:00, Raum 236 |
| Veranstaltungsnr.: | 2400094 |
| Lehrstühle: | Anwendungsorientierte Formale Verifikation Zuverlässige Softwaresysteme in der Automobilindustrie |
| Dozierende: |
Jonas Schiffl [Organisation] |
| ILIAS-Kurs: | t.b.a. |
| Anmeldung: | persönlich oder per E-Mail bei Jonas Schiffl (Raum
226, Gebäude 50.34 bzw. jonas.schiffl∂kit edu)
Anmeldeschluss: 30.10.2021 |
| Platzvergabe: | Reihenfolge nach Eingang der Anmeldung |
Themenbereich
An unserem Lehrstuhl werden formale Methoden für ein breites Spektrum moderner Softwareentwicklung erforscht.
In diesem Seminar werden verschiedene formale Techniken vorgestellt, die dazu beitragen, Programme auf ihre Korrektheit überprüfen zu können. Einige Techniken stellen neue vielversprechende Ansätze vor, andere zeigen auf wie durch geschickten Einsatz und Kombination von Heuristiken existierende Ansätze um Größenordnungen leistungsfähiger gemacht werden können.
Die vorgestellten Ansätze helfen praxisnah, Probleme in Software zu entdecken, zu vermeiden oder zu verhindern.
Aufgabenstellung
Für das Seminar werden von jedem/jeder Teilnehmer/in für eine erfolgreiche Teilnahme folgende Leistungen erwartet:- Selbständiges Erarbeiten der Inhalte des vorzustellenden Ansatzes (meist auf Basis eines Papiers im Umfang von etwa 20 Seiten). In regelmäßigen Treffen mit einem/r betreuenden Mitarbeiter/in erhalten Sie hierbei die nötige Unterstützung.
- Auswahl und Gliederung der Inhalte die in Ihrem Seminarbeitrag präsentiert werden sollen.
- Kurze Vorstellung Ihrer Gliederung im Plenum.
- Entscheidung, wie Sie die Inhalte präsentieren wollen.
- Erstellung der Folien für die Präsentation und gegebenfalls weiterer Materialien.
- 30-minütiger Hauptvortrag im Plenum (gefolgt von einer etwa 15-minütigen Diskussion).
- Nach dem Vortrag: Verfassen einer etwa zehnseitigen Ausarbeitung, die die wesentlichen Inhalte des Ansatzes und Ihres Vortrags zusammenfassend darstellt.
Vortragsthemen
Die folgende Themenliste soll eine Orientierung über mögliche Themen geben. Wir sind offen für Themenvorschläge aus den Bereichen Formale Verifikation und Methoden. Bei Fragen zu Themen oder Organisation wenden Sie sich bitte an Jonas Schiffl.
- Formal Methods for Blockchain and Smart Contracts
A Concurrent Perspective on Smart Contracts. Ilya Sergey and Aquinas Hobor, Financial Crypto 2017.
- (Linear) Types for 0, 1, or many uses
Mogensen, T.: Types for 0, 1 or many uses - Haftung und Verantwortung in einem Blockchain-System
Accountability in a Permissioned Blockchain: Formal Analysis of Hyperledger Fabric - Modellgetriebene Entwicklung von Smart Contracts
Towards Model-Driven Engineering of Smart Contracts for Cyber-Physical Systems - Modular Bug-Finding Techniques
Moy et al.: Modular Bug-finding for Integer Overflows in the Large: Sound, Efficient, Bit-precise Static Analysis. Microsoft Research Technical Report MSR-TR-2009-57
- Combining Model Checking and Deduction
Shankar, N.: Combining Model Checking and Deduction. Handbook of Model Checking. Springer 2018.
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge 1999.
Shankar, N.: Automated Deduction for Verification. ACM Comput. Surv. 41(4), 20:1–20:56 2009. - Modern Model Checking
Biere et.al. Symbolic Model Checking without BDDs.
McMillan. Interpolation and SAT-based Model Checking. - Learning Invariants with ICE and IC3
Aaron Bradley. SAT-Based Model Checking Without Unrolling.
Garg et. al. ICE: A Robust Framework for Learning Invariants. - Predicate Abstraction for Program Verification
Jhala, R., Podelski, A., Rybalchenko, A.: Predicate Abstraction for Program Verification - Safety and Termination. Handbook of Model Checking. Springer (2018).
Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 21:1–21:54 (2009).
Clarke, E.M., Kurshan, R.P., Veith, H.: The Localization Reduction and Counterexample-Guided Abstraction Refinement. Essays in Memory of Amir Pnueli 2010. Springer (2010). - Graph Neural Networks for SAT Solving
Bunz and Lamm: Graph Neural Networks and Boolean Satisfiability
- Confidentiality by Formal Methods
Sinha et al.: A design and verification methodology for secure isolated regions. PLDI 2016: 665-681
- Verification of Temporal Hyperproperties with HyperMC
- Verifikation von Sicherheitsprotokollen
Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif
The TAMARIN Prover for the Symbolic Analysis of Security Protocols
- Specification Mining
- Common Algebraic Specification Language