htw saar Piktogramm
Back to Main Page

Choose Module Version:


Shape Analysis

Module name (EN): Shape Analysis
Degree programme: Computer Science and Communication Systems, Master, ASPO 01.10.2017
Module code: KIM-SHAN
Hours per semester week / Teaching method: 2V+2P (4 hours per week)
ECTS credits: 6
Semester: 2
Mandatory course: no
Language of instruction:
Project (presentation and documentation)

[updated 26.02.2018]
Applicability / Curricular relevance:
KI844 Computer Science and Communication Systems, Master, ASPO 01.04.2016, semester 2, optional course, informatics specific
KIM-SHAN Computer Science and Communication Systems, Master, ASPO 01.10.2017, semester 2, optional course, informatics specific
PIM-WI52 Applied Informatics, Master, ASPO 01.10.2011, semester 2, optional course, informatics specific
PIM-SHAN Applied Informatics, Master, ASPO 01.10.2017, semester 2, optional course, informatics specific
60 class hours (= 45 clock hours) over a 15-week period.
The total student study time is 180 hours (equivalent to 6 ECTS credits).
There are therefore 135 hours available for class preparation and follow-up work and exam preparation.
Recommended prerequisites (modules):
Recommended as prerequisite for:
Module coordinator:
Dr.-Ing. Jörg Herter
Lecturer: Dr.-Ing. Jörg Herter

[updated 10.11.2016]
Learning outcomes:
After successfully completing this course, students will have intensified their theoretical and practical knowledge about
static program analysis techniques.
They will have an overview of different shape analysis approaches,
can differentiate between the different approaches and can
describe the analysis by means of 3-valued logic.
Students will be able to independently understand sample analyses from scientific
publications, reproduce their results
and adapt solutions from these analyses for their own
Students will be able to plan and carry out analyses independently within a group
by means of 3-valued logic and to document the resulting results.

[updated 26.02.2018]
Module content:
Shape analyses are highly comprehensive program analyses that attempt to calculate all possible (heap) memory states (which objects are created, how these objects are connected to each other [field pointers] and how they are used), which a program can achieve using the program code. An attempt is then made to derive what the program does, whether it might contain errors, and so on from this set of program states.
Unlike typical program analyses that compilers perform to detect optimization possibilities, shape analyses can for example, be used to automatically check whether a program is working correctly.
Course content:
1. Introduction/Motivation
2. Kleene´s 3-valued logic
3. Shape analysis with 3-valued logic
4. Introduction into TVLA (Three Valued Logical Analyzer)
5. Case studies and example analyses with TVLA

[updated 26.02.2018]
Recommended or required reading:
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.

[updated 26.02.2018]
Module offered in:
SS 2021, SS 2020, SS 2019, SS 2018
[Wed Dec  1 17:00:08 CET 2021, CKEY=ksa, BKEY=kim2, CID=KIM-SHAN, LANGUAGE=en, DATE=01.12.2021]