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 presents a summary of the paper.
|Instructors||Matthias Heizmann, Alexander Nutz, Christian Schilling
||Tue, 21 April 2015, 12:00-14:00 s.t., building 101, room 00-010/014|
|Presentations||Saturday, 27 June 2015; 10:30-17:00; building 101, room 01-016
|Course Catalog||Program Analysis
- The topics have been assigned. Please contact your supervisor before you read through the literature. We want to assign a specific subtopic to each of you.
- On popular demand, the date of the presentations is set to the 27th of June. Note that this is a Saturday. The exact time slots depend on the number of participants, which we will know by next Monday. Interested students should keep the day free from 10:00 to 18:00.
- Please choose three of the topics listed below and send your choices sorted according to your preferences to Christian Schilling by Sunday evening (26th April).
- Starting from Wednesday evening we will list possible seminar topics on this website. If you have a suggestion for a topic that should be covered by our seminar please let us know as soon as possible and we will (try to) include it in our list.
- In the kick-off meeting, we discussed if we can have a block seminar at the end of the semester. Unfortunately this is not possible. Nonetheless, the program analysis seminar will not be weekly Tue 12:00 - 14:00.
- The kick-off meeting takes place on Tuesday, 21 April, at 12-14 s.t.
Process of the seminar
- Participate in the kick-off meeting, where we present the available topics. Feel free to hand in your favorite topic in advance.
- 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.
- Have a meeting with your supervisor in which we discuss relevant literature and develop a very coarse sketch of your talk. (in the first weeks of the semester).
- You write a proposal in which you explain what you are going to present in your talk.
- You write an abstract of your talk.
- You submit your abstract and your proposal via email to the instructors (deadline: three weeks before your talk).
- Your proposal is reviewed by two other participants.
- You write two reviews about other participants' proposals and send them via email to the instructors (deadline: one week after you received the proposal).
- You receive reviews of your proposal (deadline: two weeks before your talk).
- You submit your slides via email to the instructors (deadline: one week before your talk).
- You have a short meeting with the instructors in which you get feedback for your slides.
- You give a ca. 30 min talk (schedule see below).
- 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 e.g.:
- 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 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 well-structured 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 any more (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 talk. 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?
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
There is not a one-to-one 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.
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.
Since the reviewes are all needed in the same week, we will assign reviewers by sending two proposals to each of you via e-mail.
- Literature: Underspecified Harnesses and Interleaved Bugs
- Talk by: Yu-Wen
- Supervisor: Alexander Nutz
- Slides: Underspecified Harnesses and Interleaved Bugs
- Literature: Danger Invariants, Flow-sensitive fault localization, Concolic Fault Abstraction , Explaining inconsistent code
- Talks by: Daniel, Numair, Sebastian
- Supervisor: Matthias Heizmann
- Slides: Explaining Inconsistent Code
- Literature: Wikipedia, Efficient Interpolant Generation in Satisfiability Modulo Theories
- Talk by: Betim
- Supervisor: Christian Schilling
- Slides: Interpolation
- Talk by: Tobias
- Supervisor: Alexander Nutz
- Literature: Mechanizing and Improving Dependency Pairs, Proving Termination and Memory Safety for
Programs with Pointer Arithmetic, Unrestricted Termination and Non-Termination Arguments for Bit-Vector Programs
- Talk by: Hannes
- Supervisor: Matthias Heizmann
- Slides: The Dependency Pair Technique - Proving Termination of Term Rewrite Systems
Verification of Multi-threaded Programs
- Talk by: Milan
- Supervisor: Alexander Nutz
Bounded Model Checking
- Literature: A solver for reachability modulo theories, Abstract Model Checking without Computing the Abstraction
- Literature: Lazy Abstraction with Interpolants
Predicate Abstraction + CEGAR
- Literature: Counter-Example Guided Abstraction Refinement
SMT / DPLL(T)
- Literature: Wikipedia, DPLL(T ): Fast Decision Procedures, Abstract DPLL and Abstract DPLL Modulo Theories
The following table contains the deadlines for the submission of the proposal, the reviews, and the slides.