MSE Research Project Database

Focused Software Testing through Backwards Program Analysis

Project Leader: Harald Sondergaard
Staff: Peter Schachte, Peter Stuckey, Graeme Gange
Collaborators: Jorge Navas, SRI International
Primary Contact: Harald Sondergaard (
Keywords: software engineering
Disciplines: Computing and Information Systems
Domains: Networks and data in society, Optimisation of resources and infrastructure

Two approaches to finding software bugs have had encouraging results. Dynamic symbolic execution (DSE) tries to improve the chances of finding bugs by systematically exploring the program from the beginning, keeping track of how the inputs forced it to take the path it took, so it can find alternative inputs that will make it take other paths. This under-approximates the set of bugs, because simply exploring all parts of the program will not necessary reveal every bug, and because it cannot always find inputs to reach every part of the program. Static analysis seeks to prove each part of the program safe for all inputs. Starting at the beginning, this approach works its way forward through the program, approximating the possible computation states at each point, looking for possible errors. Because it is impossible to precisely capture all possible states, this approach over-approximates the set of bugs, often leading to many false positives.

We wish to explore a hybrid approach, employing verification to avoid exploring parts of the program that can be proved safe, and using dynamic symbolic execution to focus on what remains. For greater effectiveness, we will develop backward analyses. Rather than starting from the beginning of the program, backward analysis starts from any potential bugs that has not been deemed harmless and works backward through the program to determine conditions that would trigger the bug, or to determine that such conditions cannot arise.

The project will create new knowledge about dynamic and static analysis of programs, and how they can work in synergy to improve testing and verification of software.