htw saar Piktogramm QR-encoded URL
Back to Main Page Choose Module Version:
emphasize objectives XML-Code

flag



Shape Analysis

Module name (EN):
Name of module in study programme. It should be precise and clear.
Shape Analysis
Degree programme:
Study Programme with validity of corresponding study regulations containing this module.
Computer Science and Communication Systems, Master, ASPO 01.10.2017
Module code: KIM-SHAN
SAP-Submodule-No.:
The exam administration creates a SAP-Submodule-No for every exam type in every module. The SAP-Submodule-No is equal for the same module in different study programs.
P222-0126
Hours per semester week / Teaching method:
The count of hours per week is a combination of lecture (V for German Vorlesung), exercise (U for Übung), practice (P) oder project (PA). For example a course of the form 2V+2U has 2 hours of lecture and 2 hours of exercise per week.
2V+2P (4 hours per week)
ECTS credits:
European Credit Transfer System. Points for successful completion of a course. Each ECTS point represents a workload of 30 hours.
6
Semester: 2
Mandatory course: no
Language of instruction:
German
Assessment:
Project (presentation and documentation)

[updated 26.02.2018]
Applicability / Curricular relevance:
All study programs (with year of the version of study regulations) containing the course.

KI844 (P221-0143) Computer Science and Communication Systems, Master, ASPO 01.04.2016 , semester 2, optional course, informatics specific
KIM-SHAN (P222-0126) Computer Science and Communication Systems, Master, ASPO 01.10.2017 , semester 2, optional course, informatics specific
PIM-WI52 (P221-0143) 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:
Workload of student for successfully completing the course. Each ECTS credit represents 30 working hours. These are the combined effort of face-to-face time, post-processing the subject of the lecture, exercises and preparation for the exam.

The total workload is distributed on the semester (01.04.-30.09. during the summer term, 01.10.-31.03. during the winter term).
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):
None.
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
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 2022, SS 2021, SS 2020, SS 2019, SS 2018 
[Sat Apr 20 13:57:45 CEST 2024, CKEY=ksa, BKEY=kim2, CID=KIM-SHAN, LANGUAGE=en, DATE=20.04.2024]