6 ECTS credits
150 h study time
Offer 1 with catalog number 4019541FNR for all students in the 2nd semester at a (F) Master - specialised level.
The goal of this course is to study automated techniques for evaluating, assuring, and improving the quality of software systems.
The initial lectures cover the static and dynamic program analyses that form the foundation for these quality assurance techniques.
1. Symbolic execution for generating tests
- Static symbolic execution: symbolic program state, SMT solving
- Dynamic symbolic execution: exploration strategies, concolic testing
2. 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
3. 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
4. Control flow and 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
5. 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
6. 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 to understand how these techniques are evolving to cope with the complexity of contemporary software. For these lectures, students prepare a presentation themselves on which they will be graded.
The goal of the practical sessions is to gain experience in implementing these techniques effectively.
Lecture slides and material for exercises are available on the learning platform.
The goals of this course are:
- Students obtain knowledge about the design of static and dynamic program analyses and their application for evaluating software quality
- Students are familiar with recent evolutions of these foundations
The corresponding learning results are:
w.r.t. knowledge:
- The student can describe the role of program analyses in the evaluation of software quality
- The student can recognise common dataflow analyses as instances of the monotone framework
- The student can motivate the need for and describe one pointer analysis for imperative programs
- The student can contrast different types of context-sensitivity for inter-procedural analyses
- The student can motivate the need for and describe one control flow analysis for higher-order programs
w.r.t. analysing:
- The student can recognise variations in the literature on foundational static and dynamic program analyses
- The student can motivate the existence of false positive and false negatives in the output of a program analysis
w.r.t. evaluating:
- The student can compare static and dynamic program analysis in terms of advantages and disadvantages
- The student can evaluate the applicability of a given program analysis for a particular software quality problem
w.r.t. creating:
- The student can independently implement logic program queries that identify instances of bug patterns and design patterns
- The student can independently extend an existing implementation of concolic testing for imperative programs
- The student can independently implement a specific dataflow analysis in a generic dataflow analysis framework
- The student is able to present a summary and comparison of recent publications in the literature
The final grade is composed based on the following categories:
Oral Exam determines 40% of the final mark.
Written Exam determines 60% of the final mark.
Within the Oral Exam category, the following assignments need to be completed:
Within the Written Exam category, the following assignments need to be completed:
Students will be graded as follows:
3 written assignments in which students explore how well existing quality assurance techniques fare in practice on realistic software (25% each),
1 oral presentation that synthesises the findings of at least two recent publications on the foundations of a particular family of techniques in the domain (25%).
The assignments and the oral presentation are mandatory and the deadlines are strict.
Failing to hand in an assignment or to present implies an absent mark for the course.
This offer is part of the following study plans:
Master of Applied Sciences and Engineering: Computer Science: Artificial Intelligence
Master of Applied Sciences and Engineering: Computer Science: Multimedia
Master of Applied Sciences and Engineering: Computer Science: Software Languages and Software Engineering
Master of Applied Sciences and Engineering: Computer Science: Data Management and Analytics