Advanced Topics in Program Analysis
Program analysis is the research area that studies the automatic analysis of computer programs. The methods that are developed in this research area, e.g., help programmers to understand complex programs, allow compilers to optimize their code, and enable computers to check the correctness of programs. In this seminar each student will study a research paper and give a talk in which he/she presents a summary of the paper.
Course type  Seminar 

Instructors  Dr. Matthias Heizmann (organization) Prof. Dr. Andreas Podelski members of the group on software engineering 
Kickoff meeting 
Friday 6th November, 14:00 c.t. in the virtual classroom in the Ilias elearning system 
Presentation language 
English 
Credits 
4 
Course Catalog  Advanced Topics in Program Analysis 
Talk dates: 
Fri 29.01.2021, Fri 5.02.2021, Fri 12.02.2021, each at 14:00 c.t. 
Room for the talks: 
Virtual classroom in the Ilias elearning system 
News and announcements
 All meetings and talks of this seminar will be held online in a virtual classroom of the Ilias elearning system.
Process of the seminar
 You participate in the kickoff meeting, where we present the available topics. Feel free to hand in your favorite topic in advance.
 You contact the instructors to obtain a topic. You may suggest a topic by yourself, pick one of the suggested topics, or find a topic suitable for you in a discussion with your supervisor.
 You have a meeting with your supervisor in which we discuss relevant literature and develop a very coarse sketch of your talk (deadline: four weeks before your talk).
 You write a proposal in which you explain what you are going to present in your talk, together with an abstract of your talk. You submit your abstract and your proposal via email to your supervisor (deadline: three weeks before your talk).
 Your proposal is reviewed by your supervisor and two other participants.
 You write two reviews about other participants' proposals and send them via email to the supervisor (deadline: one week after you received the proposal).
 You receive reviews for your proposal (deadline: two weeks before your talk).
 You submit your slides via email to your supervisor (deadline: one week before your talk).
 You have a meeting with your supervisor in which you get feedback for your slides.
 You give a talk of 30 minutes.
 You attend the talks of all other participants.
Proposals of the talk
The proposal should consist of around five pages in which you explain what you are going to present in your talk. The proposal may contain for instance:
 short overview for the reviewers (the reviewers will probably not know your topic)
 structure of your talk
 aspects of the topic that you present (why?) and ignore (why?)
 examples occurring in the talk (why these examples? Is there a running example that can be used for demonstration?)
 which definitions are presented formally? (why?), which definitions are just mentioned informally? (why?)
 which notation is used? (why?)
 which theorems are presented, which of them will be proven (why?), which proofs will be omitted (why?), will you use motivating examples in the proof?
Abstract of the talk
 one paragraph that summarizes what you present in the talk
 We will send an invitation for the seminar to all students and members of our chair. This invitation contains the abstracts of all talks.
The talk
 The goal of your talk is that the audience (master students, familiar with computer science in general, probably no experts in the topic) has the possibility to learn something new about an interesting topic. How well you achieved this goal will determine the grade of your talk.
 In a seminar you have to show that you are able to present some topic to other people. You do not have to show how well you understood the topic for yourself. How well you understood the topic has no direct influence on your grade, but only how well you presented the topic to the audience.
 You may use and copy any source of information (but do not forget to cite it). If you think your talk is just a "remix" of existing talks tailored to your audience, you might have done a great job. But do not let yourself be fooled by wellstructured and fancy talks found in the web, each talk was tailored to a specific audience.
 If you agree we put your slides on this website. Keep in mind that if you have copied images in your slides this might not be possible anymore (copyright restrictions). Of course, it will not have any effect on your grade whether we may publish your slides or not.
Review of the proposal
 Give a short summary of the talk based on the proposal (to detect misunderstandings right at the start).
 Be generous with your criticism. It is very unlikely that a student will get a bad grade because you revealed some problems in his/her proposal. However, it is very likely that a student will get a better grade if he/she was able to resolve a problem in his/her talk, thanks to your review.
 Give reasons for your criticism (e.g., "It is not possible to understand Lemma 2 because term foo was not explained."). You are also allowed to give your personal opinions, if you do so mark them as such (e.g., "Theorem 1 is very difficult to understand, in my opinion you should give an example first.").
 The following questions might be helpful to write your review
Is the proposal sufficiently well written to be readable?
Is the appearance and structure of the proposal appropriate?
Is the comprehensibility of the talk supported by relevant examples and figures?
Is the proposed structure of the talk sensible and balanced?
Are all propositions made by the author correct?
Is the line of reasoning concerning the presentation complete and accurate?
Has the author argued his/her case effectively?
Does the author use the common notation and terminology? Where would you suggest something different?
Is the schedule of the author sensible? Do you think the talk will fit into the 30 min time slot?
Grade
Your overall grade will be composed according to the following proportion.
 10% grade of your proposal
 20% grade of your reviews
 70% grade of your talk
Topics
There is not a onetoone correspondence between seminar talks and topics. Several students may give talks on the same topic, but present different aspects. The suggested literature should give you a first impression of the topics. We assign the exact literature in cooperation with you after you stated your preferences for the topic. More literature does not mean more reading, just more options. The order of appearance roughly represents the order in which it would make sense to present the topics.
If requested, some topics may also be presented in groups of two.
Some of the papers are only available via the network of our university (e.g., via vpn). If you have some problem accessing the papers, please ask us.
Constrained Horn Clauses
We can reduce verification problems to the satisfiability problem for constrained Horn clauses.
Synthesizing Software Verifiers from Proof Rules
 Talk: Milan
 Supervisor: Matthias Heizmann
 Reviewers: Max, Miriam
 Time slot: B
Checking Verification Conditions
When the program is annotated with (suitable) loop invariants, the verification problem can be reduced to passing verification conditions to a (firstorder) theorem prover. There are better and worse ways to do this.
Weakest Preconditions for Unstructured Programs
 Talk: Leon
 Supervisor: Frank Schüssele
 Reviewers: Ibrahim, Janek
 Time slot: A
Simplifying Logical Formulas
Given a logical formula, find a formula that is equivalent but smaller in size.
Small Formulas for Large Programs: OnLine Constraint Simplification in Scalable Static Analysis
 Talk: Ibrahim
 Supervisor: Matthias Heizmann
 Reviewers: Leon, Milan
 Time slot: A
Danger Invariants
Find Bugs that occur only on long program executions.
 Talk: Janek
 Supervisor: Matthias Heizmann
 Reviewers: Ibrahim, Leon
 Time slot: A
Partial Order Reduction
Efficient analysis of concurrent programs.
Dynamic Partial Order Reduction
 Talk: Mehdi
 Supervisor: Dominik Klumpp
 Reviewers: Max, Miriam
 Time slot: C
Concurrent Programs with an Unbounded Number of Threads
Efficient analysis of concurrent programs.
Thread modularity at many levels: a pearl in compositional verification (a copy is available on request) Talk: Max
 Supervisor: Jochen Hoenicke
 Reviewers: Mehdi, Milan
 Time slot: C
Loop Shrinking
Analyze loops that operate on arrays.
 Talk: Miriam
 Supervisor: Matthias Heizmann
 Reviewers: Janek, Mehdi
 Time slot: B
Schedule
Each topic/talk will have a slot letter (A, B, C) assigned.
Each seminar student has to write reviews for two other students as assigned above.
The following table contains the deadlines for the groups. Please note that "Review" stands for the review deadline for the specific group's proposals. For example if you are reviewing someone in group B, you should receive the proposal on (tbd) and send back your review on (tbd) (at the latest, the earlier the better for your reviewee)  regardless of which group your own topic is in.
Date  Proposal  Review  Slides  Talk 

08.01.2021 
A 

15.01.2021 
B 
A 

22.01.2021 
C 
B 
A 

29.01.2021 
C 
B 
A 

05.02.2021 
C 
B 

12.02.2021 
C 
Topics that Were not Assigned
Quantifier Elimination
Given a logical formula, find a quantifierfree formula that is equivalent.
Complete Integer Decision Procedures as Derived Rules in HOL Talk: tba
 Supervisor: Matthias Heizmann
 Reviewers: tba
 Time slot: tba
Loop Acceleration
Compute the transitive closure of a loop's transition relation.
A Calculus for Modular Loop Acceleration
 Talk: tba
 Supervisor: Matthias Heizmann
 Reviewers: tba
 Time slot: tba
Predicate Abstraction
Abstraction is a technique that omits details from program behaviour in order to reduce the state space that one must reason about in order to verify the program. An abstraction can be characterized by logical predicates (formulas).
Predicate abstraction for program verification
 Talk:
 Supervisor: Prof. Podelski
 Reviewers:
 Time slot: