Software Analysis

This public repository includes material (mostly slides) I prepared for a graduate course on (formal) software analysis, which I have been teaching at USI since the 2019 spring semester as part of the Master in Software and Data Engineering.

I will usually update this repository after each iteration of the course with fixes and possibly new material. You will find the material used in year 20YY in the commit tagged yYY.

Except where otherwise noted, the content is all copyright Carlo A. Furia and distributed under Creative Commons license Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0).

If you use some of this material in your own teaching, I appreciate if you drop me a line.

If you find typos or other mistakes you are welcome to post an issue (or email me if you prefer).

Topics

The course covers a variety of software analysis techniques:

1. Introduction to software analysis [slides] presents some motivation (see also here) and outlines the course's content
2. Concepts of logic and computation [slides] is a recap of formal logic and computational complexity, whose basic notions are used in the rest of the course
3. Software analysis: the very idea [slides] discusses several aspects of all software analysis techniques, which will be revisited during every main topic of the course
4. Deductive verification [slides] presents Hoare logic, deductive correctness proofs, weakest precondition calculi, verification conditions, and separation logic
5. Static analysis [slides] presents several classic dataflow analyses, gives a short high-level overview of abstract interpretation, and discusses type systems and their peculiarities as static analyses
6. Model checking [slides] includes three topics in the verification of finite-state systems: automata-based model checking (mainly with linear-time logic); software model checking using predicate abstraction; and real-time model checking using timed automata and metric temporal logic
7. Symbolic execution [slides] presents both classic symbolic execution and the more recent dynamic-symbolic execution
8. Dynamic analysis [slides] describes a variety of techniques for program analysis based on tests: delta debugging, slicing, fault localization, and assertion mining

Tools

You can try out all (open-source) tools used in the mini tutorials included in the slides by using the Docker image bugcounting/satools hosted on Docker Hub. Use the version with the same tag yYY as the corresponding GitHub tag the slides come from.

Credits

Part of the course is based on the Software Verification course that I taught with Bertrand Meyer and Sebastian Nanz at ETH Zurich in the years 2009--2015.

The closing slides in each batch reference articles and other sources on which the presentation is based.

Thanks to all students taking the course who pointed out typos and gave suggestions for improving the material.