Seminar Modular Static Analysis

Summer term 2007

J. Reineke, M.Sc., Dipl.-Inform. B. Wachter


  • 02.07.2007 Next meeting on July 11th

Important Dates

  • 25.04.2007 Assignment of papers at 16 ct. in Room 401, Building E1 3
  • 18.04.2007 Kickoff meeting at 14 ct. in Room 401, Building E1 3

General Information

This seminar focuses on the modular static analysis of software systems. Particular emphasis will be put on shape analyses coming in two flavors: based on 3-valued logic and based on separation logic. Shape analysis tries to infer precise descriptions of the shapes of data structures occuring in heap-manipulating programs. Precise shape analysis currently do not scale to larger programs in a whole-program analysis. One approach to overcome this limitation is to analyze such programs compositionally, i.e. to analyze them module by module, and to later compose the analysis results. Another motivation for modular analysis is that it allows to infer properties of a module, e.g. a library, independently of its environment (which might be unknown). We have prepared slides that give a very brief introduction into the topic and some information about the seminar.


To pass this seminar, you have to

  • give a presentation about a research paper and
  • summarize this paper in about 5 pages.


As mentioned in the requirements above, each participant has to give a presentation (45-60 minutes) about a research paper. The language of the talk is English.


Each participant has to write a detailed summary about the paper he/she presented in his/her talk.
Summaries may be written either in English or in German.

Summary Submission

The format of your summary should be pdf or postscript. Please submit within the deadlines mentioned in the schedule below (once available) to the address of your tutor. Please keep in mind, that you have to submit until 12am (12.00 CEST) at the dates given below.



Note that talks may take place later than given below. Changes will be announced on the web site.

Topic Speaker Date
Interprocedural Shape Analysis with Separated Heap Abstractions
(Tutor: Jan)
Jörg Herter May 30th
Computing Procedure Summaries for Interprocedural Analysis
(Tutor: Björn)
Mael Hörz May 30th
Using History Invariants to Verify Observers
(Tutor: Björn)
Stefan Holder June 27th
Class Invariants as Abstractions of Trace Semantics
(Tutor: Björn)
Simon Wegener June 27th
Footprint Analysis: A Shape Analysis that Discovers Preconditions
(Tutor: Jan)
Olha Honcharova July 11th
Shape Analysis For Composite Data Structures
(Tutor: Jan)
Dmytro Puzhay July 11th


Here are some suggestions on "How to give a good research talk"