Programmanalyse (Proseminar)
In this proseminar, we will study a selection of articles which can be considered classical (or fundamental) for the topic area program analysis. The articles have been published between 1938 and 2009 and some of the authors received the acknowledged Turing Award for their work.
We will have weekly sessions starting mid December (so not an "en bloc" schedule). The available topics will be introduced in the first session, together with the modus operandi (schedule, deliverables, grades).
| Course type | Proseminar |
|---|---|
| Instructors |
Prof. Dr. Andreas Podelski |
| Kickoff session | Thursday, 21 October 2021, 16:00 c.t. Online: BigBlueButton in our Ilias Course |
| Regular meetings (talks) |
Some Fridays, 14:00 - 16:00 c.t.: Online, BigBlueButton |
| Language of instruction | German |
| Credits | 3 |
| Course Catalog | Proseminar am Lehrstuhl Softwaretechnik |
| Ilias Course | Proseminar Programmanalyse |
News
- 2021-12-10: Updated location of sessions: all virtually in BBB
- 2021-11-23: Updated location of first two sessions: now virtually in BBB
- 2021-10-21: Add link to Ilias course. Update BigBlueButton link for kickoff. Update schedule.
- 2021-10-20: Update available topics, registration, process, grades, preliminary schedule.
Add BigBlueButton link for kickoff. - 2021-10-18: Update date / location for the talks.
- 2021-10-13: Website online.
Proseminar
This proseminar gives a first introduction to scientific working in the discipline of computer science. The emphasis in this proseminar is on the presentations (in the roles of speaker as well as a participant).Presentations will be on the classical 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.
Registration
- The kickoff meeting for this pro-seminar takes place at the location and time given above.
- In the kickoff meeting, we will elaborate on the goals, the construction, and the rules of the pro-seminar.
- By Monday, 25th of October 2021, 12:00 (local time), you tell us
- a list of your favourite topics (first favourite first, as many as you like)
- and that you certainly want to participate in this proseminar
- If the seminar is fully booked, we will prefer admitting students who attended the kickoff meeting and submitted their favourite topics on time. The organisors will try to match favourite topics to people as well as possible.
Sessions
The regular talk sessions take place in-person at the location and time given above.
Process of the proseminar
- If you are admitted to the proseminar, you receive an e-mail in which you are assigned to a topic and a supervisor.
- You have a meeting with your supervisor in which we discuss relevant literature and develop a very coarse sketch of your talk (ca. six weeks before your talk).
- You 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 (at least 1 working day before the next meeting).
- You have a meeting with your supervisor in which you get feedback for your proposal (ca. three weeks before your talk).
- You send your slides together with an abstract of your talk via email to your supervisor (at least 1 working day before the next meeting).
- You have a meeting with your supervisor in which you get feedback for your slides (ca. one week before your talk).
- You submit a final version of your proposal and slides via the proseminar's Ilias course (deadline: before your talk).
- You give a talk of 25 minutes.
- You receive reviews of your proposal and talk by two other participants.
- You attend the talks of all other participants.
- You write a short summary for each of the talks and submit them via the proseminar's Ilias course (deadline: one working day after each talk).
- You write two reviews about other participants' proposals and talks and submit them via the proseminar's Ilias course (deadline: one week after the talk to be reviewed).
Grade
Your overall grade will be composed according to the following proportion.
- 20% grade of your proposal
- 70% grade of your talk
- 10% grade of your reviews
Available Topics
- Alan Turing:
On Computable Numbers, with an Application to the Entscheidungsproblem. Proceedings of the London Mathematical Society. 2, 42: 230–265 (1932) - Martin Davis, George Logemann, Donald W. Loveland:
A machine program for theorem-proving. Commun. ACM 5(7): 394–397 (1962) - Tony Hoare:
An Axiomatic Basis for Computer Programming. Commun. ACM 12(10): 576–580 (1969) - Patrick Cousot, Radhia Cousot:
Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. POPL 1977: 238-252 - Amir Pnueli:The Temporal Logic of Programs. FOCS 1977: 46–57
- Edmund M. Clarke, E. Allen Emerson:
Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. Logics of Programs, Workshop, 1981, 52–71. - Randal E. Bryant:
Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Computers 35(8), 677–691 (1986). - Rajeev Alur, David L. Dill:
A Theory of Timed Automata. Theor. Comput. Sci. 126(2): 183–235 (1994) -
Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu:
Symbolic Model Checking without BDDs. TACAS 1999: 193–207 - Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani:
Automatic Predicate Abstraction of C Programs. PLDI 2001, 203–213. - Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, K. Rustan M. Leino:
Boogie: A Modular Reusable Verifier for Object-Oriented Programs. FMCO 2005, 364–387. - Matthias Heizmann, Jochen Hoenicke, Andreas Podelski:
Refinement of Trace Abstraction. SAS 2009: 69-85.
Resources
Some starting-point literature on scientific work and scientific presentations, including some pointers to further reading:
- M. Deininger, H. Lichter, J. Ludewig, K. Schneider: Studienarbeiten : ein Leitfaden zur Vorbereitung, Durchführung und Betreuung von Studien-, Diplom- und Doktorarbeiten am Beispiel Informatik. 6. Auflage. Zürich vdf (2017).
Available as e-Book via UB.
Preliminary Schedule
Each topic/talk has a group letter assigned. We have six groups in total.
The following table contains the deadlines for the groups. The dates for the meetings with your supervisor only serve as an orientation. You are responsible to make individual appointments with your supervisor. Please note that "Review" stands for the review deadline for the specific group's proposals.
| Date | Outline (Meeting) | Proposal (Meeting) | Slides (Meeting) | Prop. & Slides (Submission) | Talk- Session | Review (Submission) |
|---|---|---|---|---|---|---|
| 05. 11. 2021 | A, B | |||||
| 12. 11. 2021 |
C | |||||
| 19. 11. 2021 |
D | A | ||||
| 26. 11. 2021 |
E | B | ||||
| 03. 12. 2021 |
F | C | A | |||
| 10. 12. 2021 |
D | B | A | A | ||
| 17. 12. 2021 |
E | C | B | B | A | |
| Christmas Break | ||||||
| 14. 01. 2022 |
F | D | C | C | B | |
| 21. 01. 2022 |
E | D | D | C | ||
| 28. 01. 2022 |
F | E | E | D | ||
| 04. 02. 2022 |
F | F | E | |||
| 11. 02. 2022 | F | |||||