Inhalt

Software-Verifikation ist ein Verfahren, um Aussagen über Programme zu treffen, die die Qualität mathematischer Beweise haben. Beispiele für solche Eigenschaften sind:

• Das Programm stürzt nicht ab (z.B. durch NULL-Pointer-Exceptions)
• Das Programm enthält keine Sicherheitslücken wie z.B. Buffer Overflows
• Das Programm berechnet das richtige Ergebnis

Das Seminar befasst sich mit aktuellen Forschungsthemen auf dem Gebiet des Software-Model-Checkings und der Software-Verifikation.

Termine

Das Seminar wird als Blockveranstaltung im Juli abgehalten.

• Vorbesprechung: 19. April (14:00-15:30), Seminarraum 131
• Vorträge: 5./6. Juli

Themenvorschläge / Literatur

• Vijay Ganesh: Decision procedures for bit-vectors, arrays, and integers
• Vijay Ganesh, David L. Dill: A decision procedure for bit-vectors and arrays
• Robert Brummayer, Armin Biere: Lemmas on demand for the extensional theory of arrays
• Franjo Ivančić, Zijiang Yang, Malay K. Ganai, Aarti Gupta, Pranav Ashar: Efficient SAT-based bounded model checking for software verification
• Ernie Cohen, Michal Moskal, Stephan Tobies, Wolfram Schulte: A precise yet efficient memory model for C
• Yeting Ge, Clark Barrett, Cesare Tinelli: Solving quantified verification conditions using satisfiability modulo theories
• Roberto Bruttomesso, Natasha Sharygina: A scalable decision procedure for fixed-width bit-vectors
• Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger: Loop summarization using abstract transformers
• Adam Kiezun, Vijay Ganesh, Philip J. Guo, Pieter Hooimeijer, Michael D. Ernst: HAMPI: A Solver for string constraints