Im Seminar sind noch Plätze frei. Eine Anmeldung über das CAS-System ist bis Ende Oktober noch möglich.

Viele sicherheitskritische Systeme sind inzwischen Software-gesteuert und Software-Korrektheit daher essentiell. Andererseits ist es praktisch unmöglich, Eigenschaften eines Systems zu garantieren und die Abwesenheit von Fehlern durch Standard-Softwareengineering-Praktiken wie Code-Review, systematisches Testen und gutes Software-Design allein zu erreichen. Im Bereich der Formalen Methoden sind jedoch inzwischen verschiedene mathematische Techniken und Werkzeuge verfügbar, die eine automatische Analyse von Systemen und Software ermöglichen. Die Anwendung dieser vollautomatischen Techniken wird typischerweise algorithmische Verifikation genannt.

In diesem Seminar sollen aktuelle Arbeiten zur algorithmischen Verifikation behandelt werden, insbesondere neue Algorithmen und deren Implementation in vollautomatischen Software-Analyse-Werkzeugen. Es sollen auch Beispiele diskutiert werden, in denen diese Techniken erfolgreich angewandt wurden.

Weitere Themen des Seminars sind Verifikationsmethoden in den Bereichen Sicherheit, neuronale Netze und autonomes Fahren.

Themen

• Arie Gurfinkel, Jorge A. Navas:
  A Context-Sensitive Memory Model for Verification of C/C++ Programs. SAS 2017: 148-168
• Yakir Vizel, Arie Gurfinkel, Sharon Shoham, Sharad Malik:
  IC3 - Flipping the E in ICE. VMCAI 2017: 521-538
• 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)
• Philipp Rümmer, Hossein Hojjat, Viktor Kuncak:
  Classifying and Solving Horn Clauses for Verification. VSTTE 2013: 1-21
• Aleksandar Zeljic, Peter Backeman, Christoph M. Wintersteiger, Philipp Rümmer:
  Exploring Approximations for Floating-Point Arithmetic Using UppSAT. IJCAR 2018: 246-262
• Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy A. Mann, Pushmeet Kohli:
  A Dual Approach to Scalable Verification of Deep Networks. CoRR abs/1803.06567 (2018)
• Krishnamurthy Dvijotham, Sven Gowal, Robert Stanforth, Relja Arandjelovic, Brendan O'Donoghue, Jonathan Uesato, Pushmeet Kohli:
  Training verified learners with learned verifiers. CoRR abs/1805.10265 (2018)
• Yannick Moy, Nikolaj Bjørner, and David Sielaff:
  Modular Bug-finding for Integer Overflows in the Large: Sound, Efficient, Bit-precise Static Analysis. Microsoft Research Technical Report MSR-TR-2009-57
• Rohit Sinha, Manuel Costa, Akash Lal, Nuno P. Lopes, Sriram K. Rajamani, Sanjit A. Seshia, Kapil Vaswani:
  A design and verification methodology for secure isolated regions. PLDI 2016: 665-681
• Susmit Jha, Vasumathi Raman, Dorsa Sadigh, Sanjit A. Seshia:
  Safe Autonomy Under Perception Uncertainty Using Chance-Constrained Temporal Logic. J. Autom. Reasoning 60(1): 43-62 (2018)