htw saar
Back to Main Page

Choose Module Version:

flag

Shape Analysis

Module name (EN): Shape Analysis
Degree programme: Computer Science and Communication Systems, Master, ASPO 01.04.2016
Module code: KI844
Hours per semester week / Teaching method: 2V+2P (4 hours per week)
ECTS credits: 5
Semester: 2
Mandatory course: no
Language of instruction:
German
Assessment:
Project (presentation and documentation)
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
Workload:
60 class hours (= 45 clock hours) over a 15-week period.
The total student study time is 150 hours (equivalent to 5 ECTS credits).
There are therefore 105 hours available for class preparation and follow-up work and exam preparation.
Recommended prerequisites (modules):
KI744 Virtual Machines and Program Analysis


[updated 17.01.2008]
Recommended as prerequisite for:
Module coordinator:
Dr.-Ing. Jörg Herter
Lecturer:
Dr.-Ing. Jörg Herter


[updated 17.01.2008]
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
analyses.
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 2020, SS 2019, SS 2018, SS 2017, SS 2016, ...
[Thu Jul  9 04:10:00 CEST 2020, CKEY=ksa, BKEY=kim, CID=KI844, LANGUAGE=en, DATE=09.07.2020]