After successful completion of the course, students are able to (among others)
The course is concerned with concepts and principles of basic andadvanced approaches for the analysis and verification of softwaresystems with a focus on the concepts of soundness, completeness, andoptimality in analysis, verification and transformation. The lecturepart of the course stretches from Hoare logics to program and dataflow analysis, to the theory of abstract interpretation and tomodel-checking. Regularly assigned exercises of the tutorial part ofthe course give a hands-on experience of applying the various conceptsand principles and approaches based on them to problems and examplesthat are mostly taken from the field of optimizing and verifyingcompilation.
Part I: Motivation
Part II: Analysis and Verification
Part III: Transformation and Optimality
Part IV: Abstract Interpretation and Model-Checking
Part V: Conclusions and Prospectives
References
Appendix
Selected Reading Recommendations
ECTS Break Down:
The course is assigned 3.0 ECTS points. This corresponds to an averageworkload of 75 hours. This average workload is split among thevarious learning activities of the course as follows (the descriptions Part I to Part VI refer to the respective parts of the course notes):
The course starts with a preliminary course meeting and the first lectureon Wednesday, 4 March 2020, from 4.15pm to 5.45pm in "Hörsaal EI3a, Elektrot.Institutsg. (2nd floor)," Gußhausstr. 25-29.
Basic knowledge in theoretical computer science and programming aremandatory. Basic knowledge of compiler construction as e.g. impartedby the courses 185.A48 VU 4.0h "Compilers" or 185.A04 VU 2.0"Optimizing Compilers are useful but not strictly obligatory.
The course complements the courses 185.A04 "Optimizing Compilers"und 185.A56 "Semantics of Programming Languages." The course is thusespecially recommended for students who want to specialize in thefield of programming languages and compilers and to write e.g. a seminar or master thesis in these fields.