ECTS Breakdown:
40 hours for reading papers and related work,
20 hours for preparing the presentation,
15 hours of attending talks and meetings with the lecturer.
---------------------------------------
75 hours (3 ECTS)
---------------------------------------
PAPER ASSIGNMENT:
- Hochrainer: Verifying Properties of Binarized Deep Neural Networks
- Lachnitt: Program Analysis is Harder than Verification
- Graf: Precision-guided context sensitivity for pointer analysis
- Steinbrecher: Closed Forms for Numerical Loops
- Haupt: Counterexample-guided Inductive Synthesis Modulo Theories
- Faustmann: non-linear reasoning for invariant synthesis
- Jahn: Fast and Exact Analysis for LRU Caches
- Avdullahi: A Game-Based Approximate Verification of Deep Neural Networks with Provable Guarantees
PAPERS to choose from:
Thomas Colcombet, Joël Ouaknine, Pavel Semukhin, James Worrell:
On reachability problems for low dimensional matrix semigroups. CoRR abs/1902.09597 (2019)
Valentin Touzeau, Claire Maïza, David Monniaux, Jan Reineke:
Fast and exact analysis for LRU caches. PACMPL 3(POPL): 54:1-54:29 (2019)
Yue Li, Tian Tan, Anders Møller, Yannis Smaragdakis:
Precision-guided context sensitivity for pointer analysis. PACMPL 2(OOPSLA): 141:1-141:29 (2018)
Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin: A monadic framework for relational verification: applied to information security, program equivalence, and optimizations. CPP 2018: 130-145
Zachary Kincaid, John Cyphert, Jason Breck, Thomas W. Reps: Non-linear reasoning for invariant synthesis. PACMPL 2(POPL): 54:1-54:33 (2018)
Zachary Kincaid, Jason Breck, John Cyphert, Thomas W. Reps: Closed forms for numerical loops. PACMPL 3(POPL): 55:1-55:29 (2019)
Alessandro Abate, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen: Counterexample Guided Inductive Synthesis Modulo Theories. CAV (1) 2018: 270-288.
Min Wu, Matthew Wicker, Wenjie Ruan, Xiaowei Huang, Marta Kwiatkowska
A Game-Based Approximate Verification of Deep Neural Networks with Provable Guarantees
https://arxiv.org/pdf/1807.03571.pdf (arXiv:1807.03571v2)
Patrick Cousot, Roberto Giacobazzi and Francesco Ranzato.
Program Analysis is Harder than Verification: A Computability Perspective (CAV 2018)
Nina Narodytska, Shiva Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, Toby Walsh
Verifying Properties of Binarized Deep Neural Networks AAAI 2018
ORGANISATION:
The topics and the organization of the seminar will be discussed after an initial meeting on
Monday, April 1, 2019, 1 pm, Menger meeting room (Favoritenstrasse 9, 3rd floor)
Students signed up for the course who are unable to attend should
contact us as soon as possible.
Beachten Sie beim Verfassen der Ausarbeitung bitte die Richtlinie der TU Wien zum Umgang mit Plagiaten:
Leitfaden zum Umgang mit Plagiaten (PDF)