|Module name (EN): Shape Analysis|
|Degree programme: Applied Informatics, Master, ASPO 01.10.2011|
|Module code: PIM-WI52|
|Hours per semester week / Teaching method: 2V+2P (4 hours per week)|
|ECTS credits: 5|
|Mandatory course: no|
|Language of instruction:
Project (presentation and documentation)
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 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):
PIM-WI55 Virtual Machines and Program Analysis
|Recommended as prerequisite for:
Dr.-Ing. Jörg Herter
|Lecturer: Dr.-Ing. Jörg Herter
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.
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.
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
|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.
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.
TVLA: A framework for Kleene based static analysis.
Masterarbeit an der Universität Tel-Aviv, Israel, 2000.
|Module offered in: |
SS 2020, SS 2019, SS 2018, SS 2017, SS 2016, ...
[Sat Jul 11 12:50:30 CEST 2020, CKEY=ksa, BKEY=pim, CID=PIM-WI52, LANGUAGE=en, DATE=11.07.2020]