<?xml version="1.0" encoding="ISO-8859-1" standalone="yes" ?>
<document>
<title>Shape Analysis</title>
<cid>PIM-WI52</cid>
<sapsubmodule>P221-0143</sapsubmodule>
<bkey>pim</bkey>
<ctypes>
<hours>2</hours>
<type>V</type>
<hours>2</hours>
<type>P</type>
</ctypes>
<cp>5</cp>
<semester>2</semester>
<mandatory>nein</mandatory>
<language>Deutsch</language>
<exam>Projektarbeit (Präsentation und Dokumentation)</exam>
<curriculum>
<curriculum_entry>
<cid>KI844</cid>
<branch>Kommunikationsinformatik</branch>
<semester>2</semester>
<mandatory_tag>Wahlpflichtfach</mandatory_tag>
</curriculum_entry>
<curriculum_entry>
<cid>KIM-SHAN</cid>
<branch>Kommunikationsinformatik</branch>
<semester>2</semester>
<mandatory_tag>Wahlpflichtfach</mandatory_tag>
</curriculum_entry>
<curriculum_entry>
<cid>PIM-WI52</cid>
<branch>Praktische Informatik</branch>
<semester>2</semester>
<mandatory_tag>Wahlpflichtfach</mandatory_tag>
</curriculum_entry>
<curriculum_entry>
<cid>PIM-SHAN</cid>
<branch>Praktische Informatik</branch>
<semester>2</semester>
<mandatory_tag>Wahlpflichtfach</mandatory_tag>
</curriculum_entry>
<curriculum_entry>
<cid>PIM-SHAN</cid>
<branch>Praktische Informatik</branch>
<semester>2</semester>
<mandatory_tag>Wahlpflichtfach</mandatory_tag>
</curriculum_entry>
<curriculum_entry>
<cid>TIM-SHAN</cid>
<branch>Technische Informatik</branch>
<semester>2</semester>
<mandatory_tag>Wahlpflichtfach</mandatory_tag>
</curriculum_entry>
</curriculum>
<workload>
Die Präsenzzeit dieses Moduls umfasst bei 15 Semesterwochen 60 Veranstaltungsstunden (= 45 Zeitstunden). Der Gesamtaufwand des Moduls beträgt bei 5 Creditpoints 150 Stunden (30 Stunden/ECTS Punkt). Daher stehen für die Vor- und Nachbereitung der Veranstaltung zusammen mit der Prüfungsvorbereitung 105 Stunden zur Verfügung.
</workload>
<prerequisites>
<prerequisite>
<pfcid>PIM-WI55</pfcid>
<pftitle>Virtuelle Maschinen und Programmanalyse</pftitle>
</prerequisite>
</prerequisites>
<prerequisitesfor>
</prerequisitesfor>
<convenor>Dr.-Ing. Jörg Herter</convenor>
<convenor-person-key>jh</convenor-person-key>
<lecturers>
<lecturer>Dr.-Ing. Jörg Herter</lecturer>
<lecturer-person-key>jh</lecturer-person-key>
</lecturers>
<objectives>Die Studierenden vertiefen theoretisches und praktisches Wissen über
statische Programmanalysetechniken.
Sie haben einen Überblick über verschiedene Ansätze der &quot;Shape Analysis&quot;,
können die verschiedenen Ansätze gegeneinander abgrenzen und können
insbesondere die Analyse mittels 3-wertigen Logik beschreiben.
Die Studierenden können Beispielanalysen aus wissenschaftlichen
Veröffentlichungen selbstständig nachvollziehen, deren Ergebnisse
reproduzieren und Lösungsansätze aus diesen Analysen für eigene Analysen
adaptieren.
Die Studierenden sind in der Lage, in Gruppenarbeit eigenständig Analysen mittels
3-wertiger Logik zu planen, durchzuführen und daraus resultierende Ergebnisse zu 
dokumentieren.
</objectives>
<content>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</content>
<literature>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.</literature>
<offered>
<semshort>SS 2022</semshort>
<semshort>SS 2021</semshort>
<semshort>SS 2020</semshort>
<semshort>SS 2019</semshort>
<semshort>SS 2018</semshort>
<semshort>SS 2017</semshort>
<semshort>SS 2016</semshort>
<semshort>SS 2015</semshort>
<semshort>SS 2013</semshort>
<semshort>SS 2012</semshort>
<semshort>SS 2011</semshort>
<semshort>SS 2010</semshort>
<semshort>SS 2009</semshort>
<semshort>SS 2008</semshort>
</offered>
<moduldb-query>Sat Jul 18 20:32:53 CEST 2026, CKEY=ksa, BKEY=pim, CID=[?], LANGUAGE=de, DATE=18.07.2026</moduldb-query>
</document>
