VU Programmanalyse

Prüfungsinformationen

Die Vorlesungsteilnehmer erarbeiten einen Vortrag über ein aktuelles paper aus der Programmanalyse.

Die Vorlesungsteilnehmer nehmen aktiv an den Übungen teil. Am Anfang jeder Übung kreuzen die Vorlesungsteilnehmer an, welche Aufgaben sie in der Übung präsentieren wollen. Eine erfolgreiche Teilnahme an der Vorlesung erfordert 50% angekreuzte Aufgaben.

Liste der Vortragsthemen:

Sparse Dataflow Analysis with Pointers and Reachability, Anders Møller, Magnus Madsen, SAS 2014

Types as Abstract Interpretations, Patrick Cousot, POPL 1997 - Bernhard Gleiss

An abstract domain to infer ordinal-valued ranking function, Caterina Urban, Antoine Miné, ESOP 2014

Relational thread-modular static value analysis by abstract interpretation, Antoine Miné, SAS 2014

A Correspondence between Two Approaches to Interprocedural Analysis in the Presence of Join, Ravi Mangal, Mayur Naik, Hongseok Yang, ESOP 2014

Byte-Precise Verification of Low-Level List Manipulation, Kamil Dudka, Petr Peringer, Tomáš Vojnar, SAS 2013

Precise Relational Invariants Through Strategy Iteration, Thomas Gawlitza, Helmut Seidl, CSL 2007

Effective Static Race Detection for Java, Mayur Naik, Alex Aiken, John Whaley, PLDI 2006

Escape analysis for Java TM: Theory and practice, Bruno Blanchet, TOPLAS 2003

Die Vorträge finden in der letzten Januarwoche dieses Semesters (Jan 2015) statt. Der genau Termin wird noch bekanntgegeben.

Lernaufwand

Beschreibung

konkrete Programmanalysetechniken, der Nachweis der Korrektheit dieser Analysen mittels Abstrakter Interpretation, Techniken zur Entwicklung neuer Programmanalysen

Defintion von Syntax und Semantik einer Spielzeugsprache;
einfache Programmanalysen, die standardmäßig in Compilern eingesetzt werden, wie Reaching Definitions, Live Variable Analysis und Constant Propagation;
Programmanalysen, die zur Programmverfikation eingesetzt werden, wie Interval-, Octagon-, Polyederanalyse zur Bestimmung von Programminvarianten;
komplexere Programmanalysen, die standardmäßig in Compilern eingesetzt werden, wie Pointer Analysis und Call Graph Analysis;
fortgeschrittene Themen zur Invariantenanalyse, wie Terminations- und Boundanalyse;
die vorgestellten Programmanalysen werden mit der Methode der Abstrakten Interpretation definiert und als korrekt bewiesen, wobei die Spielzeugsprache als Referenzrahmen dient;

 

  • LVA-Nummer: 184.703
  • ECTS: 3.0
  • Stunden: 2

Module

Vortragende

Beispiele

Möchtest du die Beispiele bewerten musst du dich einloggen. Derzeit funktioniert das über Facebook, wir arbeiten an einem Login über TISS! Facebook Login

Alle Beispiele als ZIP Datei
Add files...