Program Analysis & Software Testing

News and Announcements

• (09/12/2016): Talk "Extracting Tests from Partial Verification Results" cancelled, reassigned reviewers.
• (07/11/2016): The topics and reviews have been assigned. Dates for deadlines and meetings will follow. EDIT: You can find the deadlines below.
• (04/11/2016): Hint: If you need the weekend for chosing your topic, and haven't configured VPN to the university network on your private computer yet, [here]'s the link to the instructions. (needed for many of the below links, a Google search for the title often works, too, however)
• (02/11/2016): Added slides of the introductory talk. (see below) EDIT: Now the video is there, too. Remember that we would like your topics until Friday, not until Monday, which might be said in the talk at some point. (Saturday is ok, too. Just make sure we have your E-Mail on Monday morning.)
• Please send a list of topics (at least three) in the order of your preferences to the instructors until Fri, 4 November.
  
• Besides the first ("kick-off") meeting and the introductory talk, we only meet for the student's talks, which we will announce after the topics have been assigned.
• There will be an introductory talk by the organizers on 31 October (usual time and room).
• The first meeting takes place on 17 October.

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 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 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 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

Assigned Topics

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.

Fault correlation

Wei Le, Mary Lou Soffa:
Path-based fault correlations: FSE 2010 [paper], [technical report]

Group: A

Talk: Frank

Reviewed by: Arber, Arlind

Supervisor: Christian

Local proofs

Ariel Cohen, Kedar Namjoshi:
Local proofs for global safety properties: CAV 2007 [paper]

Group: A

Talk: Arber

Reviewed by: Ravi, Arlind

Supervisor: Alexander

Information flow and security

Group: A

Talk by: Nicolas

Reviewed by: Frank, Arber

Supervisor: Alexander 

Extracting tests from partial verification results

 
Group: B

Talk: cancelled

Reviewed by: -

Supervisor: Christian

GUI testing/GUI verification

Stephan Arlt, Evren Ermis, Sergio Feo Arenis, Andreas Podelski:
Verification of GUI Applications: A Black-Box Approach. ISoLA (1) 2014: 236-252 [paper]

Group: B

Talk: Arlind

Reviewed by: Ravi, Alexander

Supervisor: Alexander

Stephan Arlt, Pedro Borromeo, Martin Schäf, Andreas Podelski:
Parameterized GUI Tests. ICTSS 2012: 247-262 [paper]

Group: B

Talk: Ravi

Reviewed by: Alexander, Sebastian

Supervisor: Alexander

Property-Directed-Reachability

Alessandro Cimatti, Alberto Griggio:
Software Model Checking via IC3. CAV 2012: 277-293 [paper]

Group: C

Talk: Alexander

Reviewed by: Sebastian, Nicolas

Supervisor: Alexander

Shape Analysis using Effectively Propositional Reasoning

Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv:
Effectively-Propositional Reasoning about Reachability in Linked Data Structures. CAV 2013: 756-772 [paper]

Group: C

Talk: Sebastian

Reviewed by: Nicolas, Frank

Supervisor: Alexander

Unassigned Topics

Data Flow Testing

On the Right Objectives of Data Flow Testing. ICST 2014: 71-80 [paper]

Interactive verification

Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham:
Ivy: safety verification by interactive generalization. PLDI 2016: 614-630 [paper]

Verification as Horn Clause Solving

Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, Andrey Rybalchenko:
Synthesizing software verifiers from proof rules. PLDI 2012: 405-416 [paper]

Theoretical Connections between Logics and Static Program Analysis

Martin Brain, Vijay D'Silva, Leopold Haller, Alberto Griggio, Daniel Kroening:
An Abstract Interpretation of DPLL(T). VMCAI 2013: 455-475 [paper]

Coverage

Thomas Ball:
A theory of predicate-complete test coverage and generation: FMCO 2005 [paper]

Additional Material

We recorded the introductory talk. [slides] [video]

Schedule

You can find the deadlines for you proposal, reviews and talk in the table below. You can find which group you and your reviewees belong to next to your topic (above).

Note that the review deadline for group A refers to when the reviews for the proposals from group A are due, e.g., if you are in group C and you are writing a review for someone in group A, you have to submit that review at 19/12/2016.