Software Analysis
People
Course director
Assistant
Description
This course describes software analysis techniques, highlights their theoretical underpinnings, and presents tools that make them available in practice to the working software engineer. The presentation includes techniques spanning different levels of correctness guarantees, automation, and applicability. The main covered topics are: axiomatic semantics and deductive verification; static analysis and type systems; model checking and predicate abstraction; symbolic execution; and dynamic analysis.
Objectives
Developing software that behaves as expected is challenging not just in practice but also due to the intrinsic complexity of analyzing software properties automatically. Software analysis offers techniques that can work around these hurdles – guaranteeing correctness, or helping find incorrect behavior.
Teaching mode
In presence
Learning methods
The course includes assignments where students apply open-source software analysis tools in practice – understanding the trade-offs involved in making software verification technology applicable in realistic settings.
Examination information
The course's grade is determined by a combination of assignments/small projects introduced during the course and about the main topics of the course, and by a final exam.
Bibliography
- Bradley, Aaron R., Manna, Zohar. The calculus of computation: decision procedures with applications to verification. Berlin: Springer, 2007.
- Huth, Michael, Ryan, Mark D, Ryan, Mark. Logic in computer science: modelling and reasoning about systems. Second edition. Cambridge: Cambridge University Press, 2004.
- Nielson, Flemming, Nielson, Hanne Riis, Riis Nielson, Hanne, Hankin, Chris. Principles of program analysis. [Corr. 2nd printing]. Berlin: Springer, 2005.
- Pierce, Benjamin C.. Types and programming languages. Cambridge Mass. London: MIT Press, 2002.
- Zeller, Andreas. Why programs fail: a guide to systematic debugging. 2nd ed., digital repr.. Amsterdam etc.]: Elsevier, 2010.
Education
- Master of Science in Informatics, Lecture, Software Development, Elective, 1st year
- Master of Science in Informatics, Lecture, Software Development, Elective, 2nd year
- Master of Science in Informatics, Lecture, Programming languages, Elective, 1st year
- Master of Science in Informatics, Lecture, Programming languages, Elective, 2nd year
- Master of Science in Software & Data Engineering, Lecture, 1st year
- PhD programme of the Faculty of Informatics, Lecture, Elective, 1st year (4.0 ECTS)
