This course is an elective at the master level, for 6 study points (26 hours lectures, 26 hours practical sessions).
The course is taught in English in the second semester.
The official course description can be found here.
About
The goal of this course is to study automated techniques for evaluating, assuring, and improving the quality of software.
Examples include
concolic testing for generating tests,
static data flow analysis for detecting bugs,
program transformation for renovating programs, and abstract interpretation for detecting security leaks.
This slide deck should give a better idea about these techniques.
A more detailed, but tentative, table of contents is as follows:
-
Symbolic execution for generating tests
- Static symbolic execution: symbolic program state, SMT solving
- Dynamic symbolic execution: exploration strategies, concolic testing
-
Program querying and transformation for detecting and repairing bugs
- Program querying: pattern characteristics, logic-based program queries, precision and recall
- Program transformation: template-based program transformations, strategic programming, search-based software engineering
-
Data flow analysis and the monotone solver
- Fixed-point theory: lattices and soundness, data flow constraints, fixed-point algorithms
- Monotone framework: forward v. backward and may v. must
-
Control flow, pointer analysis and the cubic solver
- Cubic solver: set membership constraints, cubic algorithm
- Control flow analysis: CFA for lambda-calculus, call graph construction for OO languages
- Pointer analysis: Andersen’s and Steensgard’s, null pointer analysis
-
Inter-procedural data flow analysis and the IFDS/IDE solver
- Inter-procedural control flow graphs: infeasible paths
- Context-sensitivity: cloning v. call string v. functional approach
- IFDS/IDE framework: exploded super-graph, graph reachability
-
Abstract interpretation of higher-order programs
- From operational, over collecting, to abstract semantics
- Taint analysis of Scheme for detecting security leaks
In the final lectures, we study recent publications together to understand how these foundations are evolving to cope with the complexity of contemporary software.
In the exercises, we use the TIP framework (Scala) to practice implementing static program analyses. We use the Ekeko library (Clojure) to practice program querying. We use the Kiama library (Scala) to practice program transformation.
Examination
There is no traditional oral or written exam. Students will be graded as follows:
- 3 mandatory assignments in which students apply and extend quality assurance techniques (20% each), assigned during the lectures, deadline: start of examination session.
- 1 mandatory oral presentation synthesizing two recent publications in the domain (40%), to be chosen from predetermined list, deadline: last two lectures.
Note that failing to hand in an assignment or failing to present automatically results in an ABSENT mark.
The contents of this course has moved to Canvas.