Seminar Modular Static Analysis
Summer term 2007
- 02.07.2007 Next meeting on July 11th
- 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
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.
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.
- Interprocedural Shape Analysis with Separated Heap Abstractions
- Footprint Analysis: A Shape Analysis that Discovers Preconditions
- Shape Analysis for Composite Data Structures
- Computing Procedure Summaries for Interprocedural Analysis
- Class Invariants as Abstract Interpretation of Trace Semantics
- Using History Invariants to Verify Observers
Note that talks may take place later than given below. Changes will be announced on the web site.
|Interprocedural Shape Analysis with Separated Heap Abstractions
|Jörg Herter||May 30th|
|Computing Procedure Summaries for Interprocedural Analysis
|Mael Hörz||May 30th|
|Using History Invariants to Verify Observers
|Stefan Holder||June 27th|
|Class Invariants as Abstractions of Trace Semantics
|Simon Wegener||June 27th|
|Footprint Analysis: A Shape Analysis that Discovers Preconditions
|Olha Honcharova||July 11th|
|Shape Analysis For Composite Data Structures
|Dmytro Puzhay||July 11th|
Here are some suggestions on "How to give a good research talk"