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 November (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 Marius Greitschus Tanja Schindler |
First session | Mon, 15.10.2018, 12:00 c.t. Room 101-01-018 |
Language of instruction | German |
Credits | 3 |
Course Catalog | Proseminar am Lehrstuhl Softwaretechnik |
News
- 2018-10-29: The assignment of available topics is completed. The first seminar session will take place on Nov. 26, 12:00 c.t., Room 101-01-018.
- 2018-10-15: List of available topics online.
- 2018-10-14: Proseminar homepage online.
- 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:
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. -
Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu:
Symbolic Model Checking without BDDs. TACAS 1999: 193–207 - Randal E. Bryant:
Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Computers 35(8), 677–691 (1986). - 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 - Martin Davis, George Logemann, Donald W. Loveland:
A machine program for theorem-proving. Commun. ACM 5(7): 394–397 (1962) - Edsger W. Dijkstra:
Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Commun. ACM 18(8): 453–457 (1975) - David Harel:
Statecharts: A Visual Formalism for Complex Systems. Sci. Comput. Program. 8(3): 231–274 (1987). - Matthias Heizmann, Jochen Hoenicke, Andreas Podelski:
Refinement of Trace Abstraction. SAS 2009: 69-85. - Tony Hoare:
An Axiomatic Basis for Computer Programming. Commun. ACM 12(10): 576–580 (1969) - Barbara Liskov, Jeannette M. Wing: A Behavioral Notion of Subtyping. ACM Trans. Program. Lang. Syst. 16:6 1811–1841 (1994).
- Amir Pnueli:The Temporal Logic of Programs. FOCS 1977: 46–57
- Alan Turing:
On Computable Numbers, with an Application to the Entscheidungsproblem. Proceedings of the London Mathematical Society. 2, 42: 230–265 (1932)
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.