Wintersemester 2019/2020

Anwendung Formaler Verifikation

Von der Theorie zur Anwendung

Veranstaltungstyp: Seminar
Zielgruppe: Master Informatik
Umfang: 2 SWS / 3 ECTS
Termine: Auftaktveranstaltung: 23.10.2019, 14:00, Raum 211
Kurzvorträge: 12.12.2019, 9:45, Raum 211
Hauptvorträge: 3.2.2019, 9:45, Raum 010
Veranstaltungsnr.: 2400094
Lehrstühle: Anwendungsorientierte Formale Verifikation
Zuverlässige Softwaresysteme in der Automobilindustrie
Dozierende:

Jonas Schiffl [Organisation]
Prof. B. Beckert
Prof. C. Sinz
Marko Kleine Büning
Mihai Herda
Markus Iser
Michael Kirsten
Jonas Klamroth
Dr. Mattias Ulbrich
Alexander Weigl

Anmeldung: persönlich oder per E-Mail bei Jonas Schiffl (Raum 226, Gebäude 50.34 bzw. jonas.schiffl∂kit edu)
Anmeldeschluss: 31. Oktober 2019
Platzvergabe: Reihenfolge nach Eingang der Anmeldung
Alle Plätze vergeben (15.10.2018)
Neue Anmeldungen kommen auf die Warteliste.

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.

  1. 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

  2. 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.

  3. Verification of Floating Point Algorithms

    Zeljic et al.: Exploring Approximations for Floating-Point Arithmetic Using UppSAT. IJCAR 2018: 246-262

  4. Modern Model Checking

    Biere et.al. Symbolic Model Checking without BDDs.
    McMillan. Interpolation and SAT-based Model Checking.

  5. Formula Decomposition for SAT Solving

    Heule et al.: Cube-and-Conquer for Satisfiability.

  6. Learning Invariants with ICE and IC3

    Aaron Bradley. SAT-Based Model Checking Without Unrolling.
    Garg et. al. ICE: A Robust Framework for Learning Invariants.

  7. Horn Clause Solving for Program Verification

    Bjoerner et. al. Horn Clause Solvers for Program Verification.
    Philipp Rümmer, Hossein Hojjat, Viktor Kuncak: Classifying and Solving Horn Clauses for Verification. VSTTE 2013: 1-21

  8. 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).

  9. Program Synthesis: Specification-based Creation of Programs

    Bernd Finkbeiner. Synthesis of Reactive Systems (Lecture Notes).

  10. Graph Neural Networks for SAT Solving

    Bunz and Lamm: Graph Neural Networks and Boolean Satisfiability

  11. Formal Methods in Practise

    Caitlin Sadowski, Edward Aftandilian, Alex Eagle, Liam Miller-Cushon, Ciera Jaspan: Lessons from building static analysis tools at Google. Commun. ACM 61(4): 58-66 (2018)

  12. Confidentiality by Formal Methods

    Sinha et al.: A design and verification methodology for secure isolated regions. PLDI 2016: 665-681

  13. Verification of Temporal Hyperproperties with HyperMC

    Temporal Logics for Hyperproperties. Michael Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. POST 2014.

  14. Formal Methods for Blockchain and Smart Contracts

    A Concurrent Perspective on Smart Contracts. Ilya Sergey and Aquinas Hobor, Financial Crypto 2017.

  15. Verification of C/C++ Programs

    Gurfinkel: A Context-Sensitive Memory Model for Verification of C/C++ Programs. SAS 2017: 148-168

  16. Program Slicing for Verification

    Xu et. al. A brief survey of program slicing.

  17. Reachability Modulo Theories

    Lal and Qadeer. Reachability Modulo Theories.

  18. Verification of Neural Networks

    Dvijotham et al.: A Dual Approach to Scalable Verification of Deep Networks. CoRR abs/1803.06567 (2018)
    Dvijotham et al.: Training verified learners with learned verifiers. CoRR abs/1805.10265 (2018)