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 early 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 Dr. Jochen Hoenicke Dr. Bernd Westphal Tanja Schindler Dominik Klumpp |
| First session | Monday, 21.10.2019, 10:00 c.t. Room 052-02-017 |
| Language of instruction | German |
| Credits | 3 |
| Course Catalog | Proseminar am Lehrstuhl Softwaretechnik |
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 kick-off meeting for this pro-seminar takes place at the location and time given above.
- In the kick-off meeting (and only in the kick-off meeting), we will elaborate on the goals, the construction, and the rules of the pro-seminar.
- In the kick-off meeting, there will be "pre-booking" lists which gives you a booking option.
- By Monday, 28th of October 2019, 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 you have a booking option (see above), you're in (well, up to maximum number of participants).
The organisors will try to match favourite topics to people as well as possible.
Available Topics
- Mo, 2.12.
-
-
Alan Turing:
On Computable Numbers, with an Application to the Entscheidungsproblem. Proceedings of the London Mathematical Society. 2, 42: 230–265 (1932) -
Tony Hoare:
An Axiomatic Basis for Computer Programming. Commun. ACM 12(10): 576–580 (1969)
-
Alan Turing:
- Mo, 9.12.
-
- Edsger W. Dijkstra:
Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Commun. ACM 18(8): 453–457 (1975) - 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.
- Edsger W. Dijkstra:
- Mo, 16.12.
-
- David Harel:
Statecharts: A Visual Formalism for Complex Systems. Sci. Comput. Program. 8(3): 231–274 (1987). - Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu:
Symbolic Model Checking without BDDs. TACAS 1999: 193–207
- David Harel:
- Mo, 13.1.
-
- Martin Davis, George Logemann, Donald W. Loveland:
A machine program for theorem-proving. Commun. ACM 5(7): 394–397 (1962) - Randal E. Bryant:
Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Computers 35(8), 677–691 (1986).
- Martin Davis, George Logemann, Donald W. Loveland:
- Mo, 20.1.
-
- Edmund M. Clarke, E. Allen Emerson:
Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. Logics of Programs, Workshop, 1981, 52–71. - 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
- Edmund M. Clarke, E. Allen Emerson:
- Mo, 27.1.
-
- Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani:
Automatic Predicate Abstraction of C Programs. PLDI 2001, 203–213. - Rajeev Alur, David L. Dill:
A Theory of Timed Automata. Theor. Comput. Sci. 126(2): 183–235 (1994)
- Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani:
- Mo, 3.2.
-
- Matthias Heizmann, Jochen Hoenicke, Andreas Podelski:
Refinement of Trace Abstraction. SAS 2009: 69-85. - Barbara Liskov, Jeannette M. Wing:
A Behavioral Notion of Subtyping. ACM Trans. Program. Lang. Syst. 16:6 1811–1841 (1994).
- Matthias Heizmann, Jochen Hoenicke, Andreas Podelski:
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.