Typbasierte Programmanalyse

Aktuelles

• Abgabe der Endfassung der Ausarbeitung: 14 Tage nach Vorträgen
• Erneute Terminverschiebung: Vorträge finden 2 Wochen später am Mittwoch 17.07. statt!
• Die Anmeldung zu diesem Seminar erfolgt über die zentrale Seminaranmeldung.

Inhalt

Programmanalyse beschäftigt sich mit der automatischen Entdeckung qualitativer und quantitativer Programmeigenschaften. Typische Fragen, die mit Programmanalyse beantwortet werden können, sind:  

• Welche Programmvariablen sind wann aktiv?
  (Wichtig für die Zuordnung von Speicherbereichen)
• Wieviel Speicherplatz benötigt ein Programm?
• Welchen Typ hat ein bestimmter Ausdruck?
• Welche Exceptions können von einem bestimmten Programmstück ausgelöst werden?
• Kann ein bestimmter Ausdruck den Wert "null" haben?
• Kann als geheim eingestufte Information vom Programm publik gemacht werden?

Aus der Berechenbarkeitstheorie folgt, dass alle diese Probleme in ihrer exakten Form unentscheidbar sind. Man sucht daher nach sicheren Approximationen, wie zum Beispiel eine obere Schranke an den Speicherbedarf, eine Untermenge derjenigen Ausdrücke, die nicht "null" werden, etc.

Typsysteme werden traditionell zur Beschreibung von Datentypen eingesetzt, wurden aber in letzter Zeit zu einem vielseitigen Werkzeug für die Programmanalyse weiterentwickelt.   

Im Seminar verschaffen wir uns anhand der ersten Kapitel von
   
         Nielson, Nielson, Hankin
         "Principles of Program Analysis"
         Springer, 1999
   
einen Überblick über die klassische Programmanalyse und werden anhand von
   
         Peirce
         "Advanced Topics in Types and Programming Languages"
         MIT Press, 2005
   
moderne Entwicklungen auf dem Gebiet der Typsysteme kennenlernen.

Themen

• Einführung (Seiten 1-34)
  • Bearbeitet von: Anna Beer
  • Betreuer: MH
• Kontrollflussanalyse (Seiten 141-167)
  • Bearbeitet von: Angela Peng
  • Betreuer: US
• Abstrakte Interpretation (Seiten 211-245)
  • Bearbeitet von: Florian Hoidn
  • Betreuer: US
• Typbasierte Flussanalyse (Seiten 300-318)
  • Bearbeitet von: Ignaz Karsunke
  • Betreuer: AA

• Kap. 1: Substructural Type Systems
  • Bearbeitet von: Martin Krombholz
  • Betreuer: SJ
• Kap. 2: Dependent Types
  • Bearbeitet von: Sebastian Bildner
  • Betreuer: AA
• Kap. 3: Effect Types and Region-Based Memory Management
  • Bearbeitet von: Benedikt Reschberger
  • Betreuer: MH

• Jost, Loidl, Hammond, Scaife, Hofmann. "Carbon Credits" for Resource-Bounded Computations Using Amortised Analysis, FM2009
  • Bearbeitet von: Alexander Koos
  • Betreuer: SJ

Organisation

• Umfang:  Blockseminar am Ende des Semesters
  
• Veranstalter: Prof. Dr. Martin Hofmann, Dr. Andreas Abel, Dr. Steffen Jost, Dr. Ulrich Schöpp

Anforderungen

• Blitzvortrag 90 Sekunden: Inhaltsübersicht, eine Folie
• Vortrag: 30 Minuten (plus Diskussion)
• Anwesenheit während der Seminarsitzungen
• Ausarbeitung zum Thema
  • 7000-14000 Zeichen
  • Bei Master- und Diplomstudenten werden die Anforderungen mit den Betreuern abgesprochen.

Zeit und Ort

• 30.04. 14:00 c.t. Raum L109 (Oe 67) Vorbesprechung und Themenvergabe
• 14.05. 14:00 c.t. Blitzvorträge
• bis 31.05. Treffen mit Betreuer
  
• 17.06. Abgabe der Ausarbeitung
• 24.06. Abgabe Reviews
  
• (Do, 04.07. verschoben auf) Mi, 17.07. 9-12 und 13-16 Vorträge und Diskussion
•  Mi 31.07. Abgabe Endfassung der Ausarbeitung

Weitere Informationen

Tipps zum Aufbau von Vorträgen und zu Präsentationstechniken:

• Der perfekte Seminarvortrag, A. Zeller, Universität des Saarlandes, Saarbrücken
• How to give a good research talk, S. Peyton Jones, Microsoft Research, Cambridge