htw saar Piktogramm QR-encoded URL
Zurück zur Hauptseite Version des Moduls auswählen:
Lernziele hervorheben XML-Code


Shape Analysis

Modulbezeichnung:
Bezeichnung des Moduls innerhalb des Studiengangs. Sie soll eine präzise und verständliche Überschrift des Modulinhalts darstellen.
Shape Analysis
Modulbezeichnung (engl.): Shape Analysis
Studiengang:
Studiengang mit Beginn der Gültigkeit der betreffenden ASPO-Anlage/Studienordnung des Studiengangs, in dem dieses Modul zum Studienprogramm gehört (=Start der ersten Erstsemester-Kohorte, die nach dieser Ordnung studiert).
Praktische Informatik, Master, ASPO 01.10.2017
Code: PIM-SHAN
SWS/Lehrform:
Die Anzahl der Semesterwochenstunden (SWS) wird als Zusammensetzung von Vorlesungsstunden (V), Übungsstunden (U), Praktikumsstunden (P) oder Projektarbeitsstunden (PA) angegeben. Beispielsweise besteht eine Veranstaltung der Form 2V+2U aus 2 Vorlesungsstunden und 2 Übungsstunden pro Woche.
2V+2P (4 Semesterwochenstunden)
ECTS-Punkte:
Die Anzahl der Punkte nach ECTS (Leistungspunkte, Kreditpunkte), die dem Studierenden bei erfolgreicher Ableistung des Moduls gutgeschrieben werden. Die ECTS-Punkte entscheiden über die Gewichtung des Fachs bei der Berechnung der Durchschnittsnote im Abschlusszeugnis. Jedem ECTS-Punkt entsprechen 30 studentische Arbeitsstunden (Anwesenheit, Vor- und Nachbereitung, Prüfungsvorbereitung, ggfs. Zeit zur Bearbeitung eines Projekts), verteilt über die gesamte Zeit des Semesters (26 Wochen).
6
Studiensemester: 2
Pflichtfach: nein
Arbeitssprache:
Deutsch
Prüfungsart:
Projektarbeit (Präsentation und Dokumentation)

[letzte Änderung 17.01.2008]
Verwendbarkeit / Zuordnung zum Curriculum:
Alle Studienprogramme, die das Modul enthalten mit Jahresangabe der entsprechenden Studienordnung / ASPO-Anlage.

KI844 (P221-0143) Kommunikationsinformatik, Master, ASPO 01.04.2016 , 2. Semester, Wahlpflichtfach, informatikspezifisch
KIM-SHAN (P222-0126) Kommunikationsinformatik, Master, ASPO 01.10.2017 , 2. Semester, Wahlpflichtfach, informatikspezifisch
PIM-WI52 (P221-0143) 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:
Der Arbeitsaufwand des Studierenden, der für das erfolgreiche Absolvieren eines Moduls notwendig ist, ergibt sich aus den ECTS-Punkten. Jeder ECTS-Punkt steht in der Regel für 30 Arbeitsstunden. Die Arbeitsstunden umfassen Präsenzzeit (in den Vorlesungswochen), Vor- und Nachbereitung der Vorlesung, ggfs. Abfassung einer Projektarbeit und die Vorbereitung auf die Prüfung.

Die ECTS beziehen sich auf die gesamte formale Semesterdauer (01.04.-30.09. im Sommersemester, 01.10.-31.03. im Wintersemester).
Die Präsenzzeit dieses Moduls umfasst bei 15 Semesterwochen 60 Veranstaltungsstunden (= 45 Zeitstunden). Der Gesamtumfang des Moduls beträgt bei 6 Creditpoints 180 Stunden (30 Std/ECTS). Daher stehen für die Vor- und Nachbereitung der Veranstaltung zusammen mit der Prüfungsvorbereitung 135 Stunden zur Verfügung.
Empfohlene Voraussetzungen (Module):
Keine.
Als Vorkenntnis empfohlen für Module:
Modulverantwortung:
Dr.-Ing. Jörg Herter
Dozent/innen: Dr.-Ing. Jörg Herter

[letzte Änderung 10.11.2016]
Lernziele:
Die Studierenden vertiefen theoretisches und praktisches Wissen über
statische Programmanalysetechniken.
Sie haben einen Überblick über verschiedene Ansätze der "Shape Analysis",
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.


[letzte Änderung 22.11.2017]
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 2022, SS 2021, SS 2020, SS 2019, SS 2018 
[Fri Dec 27 01:44:08 CET 2024, CKEY=ksa, BKEY=pim2, CID=PIM-SHAN, LANGUAGE=de, DATE=27.12.2024]