htw saar
Zurück zur Hauptseite

Version des Moduls auswählen:

Shape Analysis

Modulbezeichnung: Shape Analysis
Studiengang: Praktische Informatik, Master, ASPO 01.10.2011
Code: PIM-WI52
SWS/Lehrform: 2V+2P (4 Semesterwochenstunden)
ECTS-Punkte: 5
Studiensemester: 2
Pflichtfach: nein
Arbeitssprache:
Deutsch
Prüfungsart:
Projektarbeit (Präsentation und Dokumentation)
Zuordnung zum Curriculum:
KI844 Kommunikationsinformatik, Master, ASPO 01.10.2010, 2. Semester, Wahlpflichtfach, informatikspezifisch
KIM-SHAN Kommunikationsinformatik, Master, ASPO 01.10.2017, 2. Semester, Wahlpflichtfach, informatikspezifisch
PIM-WI52 Praktische Informatik, Master, ASPO 01.10.2011, 2. Semester, Wahlpflichtfach, informatikspezifisch
PIM-SHAN Praktische Informatik, Master, ASPO 01.10.2017, 2. Semester, Wahlpflichtfach, informatikspezifisch
Arbeitsaufwand:
Die Präsenzzeit dieses Moduls umfasst bei 15 Semesterwochen 60 Stunden. Der Gesamtumfang des Moduls beträgt bei 5 Creditpoints 150 Stunden. Daher stehen für die Vor- und Nachbereitung der Veranstaltung zusammen mit der Prüfungsvorbereitung 90 Stunden zur Verfügung.
Empfohlene Voraussetzungen (Module):
PIM-WI55 Virtuelle Maschinen und Programmanalyse


[letzte Änderung 17.01.2008]
Als Vorkenntnis empfohlen für Module:
Modulverantwortung:
Dr.-Ing. Jörg Herter
Dozent: Dr.-Ing. Jörg Herter

[letzte Änderung 17.01.2008]
Lernziele:
Vertiefung von theoretischem und praktischem Wissen über Programmanalyse-Techniken
Kennenlernen verschiedener Ansätze der Shape Analysis
Kennenlernen der 3-wertigen Logik
Detaillierteres Wissen über die Shape Analysis mittels 3-wertiger Logik
Nachvollziehen von Beispielanalysen
Selbstständige Planung und Durchführung von (Shape) Analysen

[letzte Änderung 17.01.2008]
Inhalt:
Shape Analysen sind sehr umfangreiche statische Programmanalysen, die versuchen alle möglichen (Heap-)Speicherzustände (welche Objekte werden angelegt, wie sind diese Objekte miteinander verbunden [Feldzeiger] und wie werden sie benutzt), die ein Programm erreichen kann anhand des Programmcodes zu berechnen. Aus dieser Menge von Programmzuständen wird dann versucht, abzuleiten, was das Programm tut, ob es möglicherweise Fehler enthält usw.
Im Gegensatz zu den typischen Programmanalysen, die Compiler durchführen, um Optimierungsmöglichkeiten zu entdecken, können Shape Analysen benutzt werden, um z.B. automatisch zu prüfen, ob ein Programm korrekt arbeitet.
 
Inhaltsübersicht:
1.Einleitung/Motivation
2.Kleenes 3-wertige Logik
3.Shape Analysis mit 3-wertiger Logik
4.Einführung in TVLA (Three Valued Logical Analyzer)
5.Fallstudien und Beispielanalysen mit TVLA

[letzte Änderung 08.02.2012]
Literatur:
Mooly Sagiv, Thomas Reps und Reinhard Wilhelm:
Parametric Shape Analysis via 3-Valued Logic
ACM Transactions on Programming Languages and Systems, 2002.
 
Jan Reineke:
Shape Analysis of Sets.
Masterarbeit an der Universität des Saarlandes, 2005.
 
Tal Lev-Ami, Thomas W. Reps, Mooly Sagiv und Reinhard Wilhelm:
Putting static analysis to work for verification: A case study.
ISSTA 2000: 26-38.
 
Tal Lev-Ami und Mooly Sagiv:
TVLA: A System for Implementing Static Analyses.
SAS 2000: 280-301.
 
Tal Lev-Ami:
TVLA: A framework for Kleene based static analysis.
Masterarbeit an der Universität Tel-Aviv, Israel, 2000.

[letzte Änderung 20.07.2011]
Modul angeboten in Semester:
SS 2017, SS 2016, SS 2015, SS 2013, SS 2012, ...
[Mon Sep 25 04:34:32 CEST 2017, CKEY=ksa, BKEY=pim, CID=PIM-WI52, LANGUAGE=de, DATE=25.09.2017]