Seminar Zeigeranalyse (Pointer Analysis)

Wintersemester 2006/07
Betreuer: Katoen, Noll, Rieger, Ábrahám
Plätze: 15
Art der Veranstaltung: Theorie-/Vertiefungsseminar (wöchentlicher Vortrag)
Termin: wird bekanntgegeben

Inhalt des Seminars

Zeiger sind ein mächtiges und sehr flexibles Programmierkonzept aber gleichzeitig fehleranfällig dadurch, daß durch mehrere Referenzen auf eine Speicherzelle Abhängigkeiten im Programm entstehen können, die auf den ersten Blick nicht sofort ersichtlich sind. Die Folge sind z.B. Speicherzugriffsfehler zur Laufzeit, deren Erkennung durch Typsysteme nicht gewährleistet werden kann.

In heutigen objektorientierten Programmiersprachen sind Zeiger auf Objekte und Referenzen/Abhängigkeiten zwischen Objekten allgegenwärtig, auch wenn sie teilweise implizit verwendet werden.

Teilnahmebedingungen

Vordiplom oder Bachelor in Informatik

Ort und Zeit

Ort: Seminarraum des Lehrstuhls Informatik 2 (Raum 4201b)
Wochentag: Donnerstag
Zeitpunkt: 10:00 Uhr
Erster Termin: 19.10.2006

Organisatorisches

Jeder Teilnehmer bearbeitet ein Thema.
Ca. 15 Seiten Ausarbeitung
45 min Vortrag
Deutsch oder englisch
Wöchentlicher Termin

Zeitplan

sofort: Literaturbeschaffung (aus dem Netz, der Bibliothek oder vom Betreuer)
6 Wochen vor dem Vortrag: Besprechung der Ausarbeitung mit dem Betreuer
2 Wochen vor dem Vortrag: Endgültige Version der Ausarbeitung liegt vor.
1 Woche vor dem Vortrag: Besprechung des Vortrags mit dem Betreuer (Vorstellung der Folien)

Themen / Literatur

Nr.	Datum	Download	Titel	Seminarist(in)	Betreuer
Heapabstraktion
2	26.10.06	[pdf]	Andreas Podelski, Thomas Wies: Boolean Heaps. SAS 2005: 268-283	Plücker	TN
3	02.11.06	[pdf]	Roman Manevich, Eran Yahav, Ganesan Ramalingam, Shmuel Sagiv: Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. VMCAI 2005: 181-198	Weise	TN
4	~~09.11.06~~ ENTFÄLLT!	[pdf]	~~Erika Abraham, Andreas Gruner, Martin Steffen: Heap-abstractions for an object-oriented calculus with thread classes. COSMICAH 2005.~~	~~Wolf~~	EA
Historisches
1	~~16.11.06~~ ENTFÄLLT	~~[pdf]~~	~~Greg Nelson: Verifying Reachability Invariants of Linked Structures. POPL 1983: 38-47~~	~~El Majdoubi~~	TN
Hoare-Logik
6	23.11.06	[pdf]	Cristiano Calcagno, Samin S. Ishtiaq, Peter W. O'Hearn: Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic. PPDP 2000: 190-201	Schanen	SR
7	30.11.06	[pdf]	Pascal Fradet, Ronan Caugne, Daniel Le Métayer: Static Detection of Pointer Errors: An Axiomatisation and a Checking Algorithm. ESOP 1996: 125-140	Wetzel	TN
Separation Logic
8	~~07.12.06~~ ENTFÄLLT!	[pdf]	~~John C. Reynolds: Separation Logic: A Logic for Shared Mutable Data Structures. LICS 2002: 55-74~~	~~Rodrigues Lé~~	SR
9	~~14.12.06~~ ENTFÄLLT!	[pdf]	~~Peter W. O'Hearn: Resources, Concurrency and Local Reasoning, to appear in Theoretical Computer Science, 2006.~~	~~Clermont~~	~~JPK~~
10	11.01.07 Doppelvortrag	[pdf]	Stephen D. Brookes: A Semantics for Concurrent Separation Logic. CONCUR 2004: 16-34	von Styp-Rekowski	JPK
Temporale Logik
11	11.01.07 Doppelvortrag	[pdf]	Eran Yahav, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm: Verifying Temporal Heap Properties Specified via Evolution Logic. ESOP 2003: 204-222	Weber	JPK
Baumstrukturen und nebenläufige Listen
12	18.01.07	[pdf]	Peter Habermehl, Radu Iosif, Tomás Vojnar: Automata-Based Verification of Programs with Tree Updates. TACAS 2006: 350-364	Jansen	EA
13	25.01.07	[pdf]	Tuba Yavuz-Kahveci, Tevfik Bultan: Automated Verification of Concurrent Linked Lists with Counters. SAS 2002: 69-84	Krassnigg	SR
14	01.02.07	[pdf]	P. Baldan, A. Corradini, J. Esparza, T. Heindel, B. Konig, V. Kozioura: Verifying Red-Black Trees. COSMICAH 2005.	Felger	TN
15	08.02.07	[pdf]	Alexey Loginov, Thomas Reps and Mooly Sagiv: Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm, SAS 2006	Ißler	SR

Betreuer

JPK: Prof. Dr. Joost-Pieter Katoen, katoen[at]cs.rwth-aachen.de, Raum 4214
TN: Dr. Thomas Noll, noll[at]cs.rwth-aachen.de, Raum 4211
SR: Stefan Rieger, rieger[at]cs.rwth-aachen.de, Raum 4206
EA: Dr. Erika Ábrahám, eab[at]informatik.rwth-aachen.de, Raum 4201