You are here: Home › Teaching › Winter Term 2022/23 › Programanalysis and Verification …

Program Analysis and Verification (Seminar)

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

Prof. Dr. Andreas Podelski
Dr. Matthias Heizmann
Elisabeth Henkel (contact person for organizational matters)
Kickoff session Friday, 21. October 2022, 10:00 c.t. (online)
BigBlueButton
Talk session

Wednesday 15. February 2023, 10:00 -18:00 s.t. (in-person)
(Building 106, SR 00 007)
Language of instruction English
Credits 4
Course Catalog Program Analysis and Verification
Ilias Course Students registered on HisInOne will be added to the course automatically.
 

News

  • Feb 1:Add room for talk session
  • Oct 19: Add BBB link.
  • Oct 11: Website online.

Seminar

This seminar gives a first introduction to scientific working in the discipline of computer science. The emphasis in this seminar is on the presentations (in the roles of a speaker as well as a participant).
Presentations will be on articles from the topic area of program analysis as listed below, focusing on particular aspects of the articles. In the end, for each presentation the focus will be set in a way that all topics have a similar difficulty.
You get a first impression on the content of the seminar by looking at the papers (see below). To attend the seminar, and to read the papers, it will help if you have attended a lecture on program verification (such as the one in the summer semester).

Registration

  • In order to assign the topics, we would like to hear about your background knowledge.
    Here is a list of keywords that are relevant for one or more topics of the seminar.
    Please send an email to heizmann@informatik.uni-freiburg.de and mention all keywords that you are familiar with.
    We would be happy to receive your email before the kick-off meeting.
    Concurrent programs, Petri nets, Abstract interpretation, Craig interpolants, Linear time logic (LTL), Büchi automata, Nested word automata, Hoare logic, Assertions, Inductive invariants, First-order logic, control-flow graphs, partial-order reduction, liveness, ranking functions
  • The kickoff meeting for this seminar takes place online (BigBlueButton) at the time given above.
  • In the kickoff meeting, we will elaborate on the goals, the construction, and the rules of the seminar.
  • By Monday, 24th of October 2022, 09:00 (local time), you tell us that you certainly want to participate in this seminar and tell us your list of keywords.
  • If the seminar is fully booked, we will prefer admitting students who attended the kickoff meeting and told us via email that they want to participate.

Sessions

The regular talk sessions take place in-person as a block seminar at the location and time given above.

Process of the seminar

  • If you are admitted to the seminar, you receive an e-mail in which you are assigned to a paper and a supervisor.
  • You read your paper and write a proposal in which you explain what you are going to present in your talk. You send your proposal via email to your supervisor.
  • You have a meeting with your supervisor in which you get feedback on your proposal.
  • You submit a final version of your proposal via the seminar's Ilias course.
  • You receive the proposals of the other participants.
  • You write a review for the proposal of one participant and do some preparation for the talk sessions (see below).
  • You submit your preparation via the seminar's Ilias course.
  • You send your slides via email to your supervisor.
  • You have a meeting with your supervisor in which you get feedback for your slides.
  • You submit a final version of your slides via the seminar's Ilias course.
  • You give a talk of 25 minutes and answer questions in the subsequent discussion round (5 - 10 minutes).
  • You attend the talks of all other participants and participate in the discussion rounds.

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 should contain at least:

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

Short Summary & Questions

  • You read the proposals of all other participants.
  • For each proposal you write a short summary (2-3 sentences).
  • For each proposal you write down two precise questions that you may ask the speaker after the talk was given.

Grade

Your overall grade will be composed according to the following proportion.

  • 33.3% grade of your proposal
  • 33.3% grade of your slides and talk
  • 33.3% grade of your session preparation

Available Topics

 

Preliminary Schedule

The following table contains the preliminary schedule. The dates for the meetings with your supervisor only serve as an orientation. You are responsible to make individual appointments with your supervisor.

DateMeetings
SubmissionsEvents
20.10.22
 Kickoff (online)
30.10.22
 Topic Assignment
13.01.23
 Proposal
20.01.23
 Proposal
23.01.23 Handout of Proposals
03.02.23
Slides
10.02.23

Slides
Short Summaries & Questions
15.02.23 Talk session (in-person)