The seminar covers selected topics in the field of automated software
verification. The course revolves around seminal research papers
in the field of software verification and state-of-the-art techniques
based on these papers. Each student will be assigned two research
papers: one seminal publication of historical relevance, and a more
recent paper on the same topic. The students are expected to read and
understand the papers and prepare and present a half-hour talk on the
topic. In addition, a 1-2 pages written on the topic is also required.
The first objective is to read and understand the content as well
as the (historical) significance of the assigned papers, as well as to
locate and read up on related work if the papers are 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;
- to discuss the advances since the publication of the earlier paper;
- to summarize the papers in a short written report.
Requirements on the presentation:
- One third of the presentation should follow a popular science style presentatiom. It should put the importance of the paper in a larger context, describing its potential impact on the society and its influence on the scientific community. This part of the presentation should be addressed to the general public.
- About two thirds of the presentation should be dedicated to the scientific/technical content of the original papers. This part of the presentation should be addressed to computer scientists.
Students are required to present and discuss their slides with the lecturer prior
to giving the presentation.
Requirements on the written report: The written report should summarize the papers in 1-2 pages, explaining the impact and importance of the papers and overviewing their main technical contributions. Personal reflections on the papers are highly recommended.
ECTS Breakdown:
40 hours for reading papers and related work,
20 hours for preparing the presentation and report,
15 hours of attending lectures, talks and meetings with the lecturer.
---------------------------------------
75 hours (3 ECTS)
---------------------------------------
ORGANISATION:
The seminar will start with two lectures in which scientific principles and advices are discussed for reading and searching literature and making scientific presentations. The first two lectures of the seminar will take place as follows:
Lecture 1: Introductory lecture on November 7, 2pm, Hahn seminar room (Favoritenstrasse 9, 3rd floor)
Lecture 2: November 9, 2pm, Menger seminar room (Favoritenstrasse 9, 3rd floor)
Papers are assigned to students after the second seminar lecture on November 9.
Students are expected to read assigned papers, search relevant literature and prepare scientific presentation on the paper. The remaining seminar events will host student presentations.
Students signed up for the course who are unable to attend should
contact us as soon as possible (email laura.kovacs@tuwien.ac.at).
Electronic versions of the papers will be provided to the students.
All presentations will take place mid December.
RESOURCES:
How to give a good talk (by Simon Peyton Jones, given in Vienna, October 2004):
http://research.microsoft.com/en-us/um/people/simonpj/papers/giving-a-talk/giving-a-talk.htm
(requires Real Player)
PAPERS:
Seminal papers:
1. Ken McMillan."Interpolation and SAT-Based Model Checking". Computer Aided Verification (CAV), 2003. [pdf]
2. Ranjit Jhala and Ken McMillan. "A Practical and Complete Approach to Predicate Refinement". Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2006. [pdf]
3. Sriram Sankaranarayanan, Henny Sipma and Zohar Manna. "Non-linear Loop Invariant Generation using Gröbner bases". Principles of Programming Languages (POPL), 2004. [pdf]
Recent papers:
4. Azadeh Farzan and Zachary Kincaid. "Compositional Recurrence Analysis". Formal Methods in Computer Aided Design (FMCAD), 2015. [pdf]
5. Rahul Sharma, Isil Dillig, Thomas Dillig and Alex Aiken. "Simplifying Loop Invariant Generation Using Splitter Predicates". Computer Aided Verification (CAV), 2011. [pdf]
6. Alastair F. Donaldson, Leopold Haller, Daniel Kroening, and Philipp Rümme r. "Software Verification Using k-Induction". Static Analysis Symposium (SAS), 2011. [pdf]
7. Yakir Vizel, Arie Gurfinkel and Sharad Malik. "Fast Interpolating BMC". Computer Aided Verification (CAV), 2015. [pdf]
8. Dirk Beyer and Stefan Löwe. "Explicit-State Software Model Checking Based on CEGAR and Interpolation". Fundamental Approaches to Software Engineering (FASE), 2013. [pdf]
Paper selection:
Students should select two paper for reading, presenting and summarizing. One paper should be a seminal paper, that is one of papers 1-3 above. The other paper should be a more recent papers, that is from papers 4-8 above, reporting recent results on the research started in the seminal paper.
- When choosing one of papers 1-2 above, students should choose another paper from papers 6-8.
- When choosing paper 3, students should choose another paper from papers 4-5.
Paper assignments to students:
1. Kreshnik Zuberi - assigned papers:
- Ken McMillan."Interpolation and SAT-Based Model Checking". Computer Aided Verification (CAV).
- Yakir Vizel, Arie Gurfinkel and Sharad Malik. "Fast Interpolating BMC". Computer Aided Verification (CAV)
2. Zhang Fenghong - assigned papers:
- Sriram Sankaranarayanan, Henny Sipma and Zohar Manna. "Non-linear Loop Invariant Generation using Gröbner bases". Principles of Programming Languages (POPL), 2004
- Azadeh Farzan and Zachary Kincaid. "Compositional Recurrence Analysis". Formal Methods in Computer Aided Design (FMCAD), 2015
3. Thomas Brandstätter - assigned papers:
- Ranjit Jhala and Ken McMillan. "A Practical and Complete Approach to Predicate Refinement". Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2006
- Dirk Beyer and Stefan Löwe. "Explicit-State Software Model Checking Based on CEGAR and Interpolation". Fundamental Approaches to Software Engineering (FASE), 2013
4. Jaiswal Kanishk Raj - assigned papers:
- Ken McMillan."Interpolation and SAT-Based Model Checking". Computer Aided Verification (CAV)
- Yakir Vizel, Arie Gurfinkel and Sharad Malik. "Fast Interpolating BMC". Computer Aided Verification (CAV)
Beachten Sie beim Verfassen der Ausarbeitung bitte die Richtlinie der TU Wien zum Umgang mit Plagiaten:
Leitfaden zum Umgang mit Plagiaten (PDF)Beachten Sie beim Verfassen der Ausarbeitung bitte die Richtlinie der TU Wien zum Umgang mit Plagiaten:
Leitfaden zum Umgang mit Plagiaten (PDF)
The oral exam will taken place on December 14, between 10:00-12 o'clock and 13:00-15:00, in Seminar room Hahn (Favoritenstrasse 9-11, 3rd floor).
The schedule for the examination is as follows:
- 10:00-11:00: Kreshnik Zuberi
- 11:00-12:00: Zhang Fenghong
- 13:00-14:00: Jaiswal Kanishk Raj
- 14:00-15:00: Thomas Brandstätter
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 be counted in 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, give own intuition, reflect on the paper) will count for the grade.
3.) The written report will also count in the final grade.
Additional information on grading: The grade on the presentation will count 80% of the final grade, while the written report will count for 20% of the final grade.
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). Attendance of
the meetings is compulsory - not showing up may affect your grade.
