You are here: Home Teaching Winter Term 2018/19 Programmanalyse (Proseminar)

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


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

Available Topics

  1. Rajeev Alur, David L. Dill:
    A Theory of Timed Automata.
    Theor. Comput. Sci. 126(2): 183–235 (1994)
  2. Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani:
    Automatic Predicate Abstraction of C Programs. PLDI 2001, 203–213.
  3. Michael BarnettBor-Yuh Evan ChangRobert DeLineBart JacobsK. Rustan M. Leino:
    Boogie: A Modular Reusable Verifier for Object-Oriented Programs. FMCO 2005, 364–387.
  4. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu:
    Symbolic Model Checking without BDDs. TACAS 1999: 193–207
  5. Randal E. Bryant:
    Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Computers 35(8), 677–691 (1986).
  6. Edmund M. ClarkeE. Allen Emerson:
    Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. Logics of Programs, Workshop, 1981, 52–71.
  7. 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
  8. Martin Davis, George Logemann, Donald W. Loveland:
    A machine program for theorem-proving. Commun. ACM 5(7): 394–397 (1962)
  9. Edsger W. Dijkstra:
    Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Commun. ACM 18(8): 453–457 (1975)
  10. David Harel:
    Statecharts: A Visual Formalism for Complex Systems. Sci. Comput. Program. 8(3): 231–274 (1987).
  11. Matthias Heizmann, Jochen Hoenicke, Andreas Podelski:
    Refinement of Trace Abstraction. SAS 2009: 69-85.
  12. Tony Hoare:
    An Axiomatic Basis for Computer Programming. Commun. ACM 12(10): 576–580 (1969)
  13. Barbara Liskov, Jeannette M. Wing: A Behavioral Notion of Subtyping. ACM Trans. Program. Lang. Syst. 16:6 1811–1841 (1994).
  14. Amir Pnueli:
    The Temporal Logic of Programs. FOCS 1977: 46–57
  15. Alan Turing:
    On Computable Numbers, with an Application to the Entscheidungsproblem. Proceedings of the London Mathematical Society. 2, 42: 230–265 (1932)



Some starting-point literature on scientific work and scientific presentations, including some pointers to further reading: