|
Lehrende: Prof. Dr. rer. nat. Marie-Christine Jakobs
Veranstaltungsart:
Integrierte Veranstaltung
Orga-Einheit: FB20 Informatik
Anzeige im Stundenplan:
ASV
Fach:
Anrechenbar für:
Semesterwochenstunden:
4
Unterrichtssprache:
Englisch
Min. | Max. Teilnehmerzahl:
- | -
Digitale Lehre:
Dieses Semester findet der Kurs online statt. Den Kursinhalt erarbeiten Sie sich hauptsächlich im Selbststudium. Eine wöchentliche Fragestunde erlaubt es Ihnen sich mit der Dozentin und anderen Kursteilnehmern auszutasuchen. Darüber hinaus gibt es weitere asynchrone Angebote um Feedback zu bekommen und Fragen zu stellen.
Di 12:00-13::00, Zoom Fragestunde
Unser erstes Online-Treffen ist am 13.04.2021 um 11:45 Uhr, um die Organisation des Kurses zu besprechen.
Details finden Sie im Moodle Kurs: https://moodle.informatik.tu-darmstadt.de/course/view.php?id=1029
Lehrinhalte:
Die Veranstaltung befasst sich mit den Techniken zur automatischen Softwareverifikation und behandelt dabei folgende Themebereiche:
- operationelle Semantik von sequentiellen Programmen
- konfigurierbare Programmanalyse inklusive Konfiguration für Datenflussanalysen und Model Checking
- counter-example guided abstraction refinement (CEGAR)
- Bounded Model Checking
- k-Induktion
- kooperative Verifikation, insbesondere Conditional Model Checking
Literatur:
Semantik
- K. R. Apt, F. S. de Boer, E.-R. Olderog: Verification of Sequential and Concurrent Programs. Springer 2009.
- Edsger W. Dijkstra: A Discipline of Programming, Prentice-Hall, 1976.
Domänen, Programmanalyse, Model Checking, CEGAR
- E. M. Clarke, T.A. Henzinger, H. Veith, R. Bloem: Handbook of Model Checking, Springer, 2018.
- D. Beyer D., T. A. Henzinger, G. Théoduloz G.: Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis, CAV, LNCS 4590, pp. 504-518, Springer, 2007.
- Ranjit Jhala and Rupak Majumdar. Software model checking. ACM Comput. Surv. 41, 4, Article 21, 2009.
- D. Beyer, S. Löwe: Explicit-State Software Model Checking Based on CEGAR and Interpolation, FASE, LNCS 7793, pp. 146-162, Springer, 2013.
- F. Nielson, H. R. Nielson, C. Hankin. Principles of Program Analysis, Springer, 2009.
- T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre: Lazy abstraction, POPL, pp. 58-70, ACM, 2002.
- D. Beyer, S. Löwe, P. Wendler: Sliced Path Prefixes: An Effective Method to Enable Refinement Selection, FORTE, LNCS 9039, pp. 228-243, Springer, 2015.
- D. Beyer, A. Cimatti, A. Griggio, M. E. Keremoglu, R. Sebastiani: Software model checking via large-block encoding, FMCAD, pp. 25-32, IEEE, 2009.
- M. Heizmann , J. Hoenicke, A. Podelski: Refinement of Trace Abstraction, SAS, LNCS 5673, pp. 69-85, Springer, 2009.
Bounded Model Checking, k-Induktion
- A. Biere, A. Cimatti, E. Clarke, O. Strichman, Y. Zhu: Bounded model checking, Advances in computers 58 (11), Academic Press, 2003.
- E. Clarke, D. Kroening, K. Yorav: Behavioral consistency of C and Verilog programs using bounded model checking, DAC, pp. 368-371, ACM, 2003.
- A. F. Donaldson, L. Haller, D. Kroening, P. Rümmer: Software Verification Using k-Induction, SAS, LNCS 6887, pp. 351-368, Springer, 2011.
Conditional Model Checking
- D. Beyer, T. A. Henzinger, M. Erkan Keremoglu, P. Wendler: Conditional model checking: a technique to pass information between verifiers, FSE, ACM, 2012.
- D. Beyer, M.-C. Jakobs, T. Lemberger, H. Wehrheim: Reducer-based construction of conditional verifiers, ICSE, pp. 1182-1193, ACM, 2018.
Voraussetzungen:
Empfohlen:
Informatikkenntnisse entsprechend der ersten vier Semester des Bachelorstudiengangs Informatik, insbesondere Kenntnisse aus der Vorlesung Aussagen und Prädikatenlogik oder Vergleichbares.
Online-Angebote:
https://moodle.informatik.tu-darmstadt.de/course/view.php?id=1029
|
