Reading of scientific papers,
literature research,
presentation of scientific work

The seminar covers selected topics in the field of formal methods. The course revolves around seminal research papers in the field of automated reasoning and computer-aided verification.  Each student will be assigned one research papers. The students are expected to read and understand the paper and prepare and present a half-hour talk on the topic. 

The first objective is to read and understand the content as well as the significance of the assigned paper, and read up on related work if the paper is not self-contained.
Prior to preparing the presentation, students are expected to discuss the papers in a meeting with the lecturer.

The objectives of the presentation are to present the topic in a manner accessible for their fellow students. Students are required to present and discuss their slides with the lecturer prior to giving the presentation.

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. 

Students will be graded based on:

1.) Ability to read and understand the papers assigned to them. The
effort and initiative to independently read and understand the paper
and to read up on related work will determine 50% of the grade. The
students' understanding of the paper will be evaluated during the
meetings with the lecturer and by means of questions after the talk.

2.) Ability to present the material in an accessible way to their fellow
students. The clarity and style of the presentation as well as the
students' effort to prepare the talk (e.g., by designing their own
examples rather than reusing material from the paper) determine 50% of
the grade.

Additional information on grading: The relative difficulty of the
paper will be taken into account. Asking meaningful questions about
the presentations of fellow students will have a positive impact
on the grade (attendance of these talks is compulsory).

Slides of the Introductory lecture from April 1, 2019 are online.