Reusing Solutions Modulo Theories

You are cordially invited to attend the PhD Dissertation Defense of Andrea AQUINO on Friday, March 16th 2018 at 15h30 in room SI-008 (Informatics building)

Abstract:
Symbolic program analysis techniques have been employed since the early seventies to verify properties of programs. Nowadays, these techniques play an important role in the verification of a wide range of software systems, including wireless sensor networks, distributed systems, the firmware of medical devices and the drivers of popular operating systems.
Symbolic program analysis techniques generate formulas describing the behaviour of a subject program. They rely on Satisfiability Modulo Theories (SMT) solvers to determine the satisfiability of these formulas and use this information to determine whether the program under analysis satisfies some properties of interest.
Despite the remarkable progress made in the development of such tools, SMT solvers still represent a main bottleneck to the scalability of many modern symbolic program analysis techniques.
To mitigate the impact of constraint solvers on the cost of program analysis, researches have designed different approaches that store and reuse the solutions of formulas generated during the analysis of a program to determine the satisfiability or the unsatisfiability of formulas generated at later stages of the analysis of that program, without relying on possibly expensive calls to constraint solvers.
In this thesis, we propose an original approach of this kind that can identify more reuse opportunities than other state-of-the-art approaches and that can be applied to more logics. To this end, we start by introducing the concept of symbolic program analysis and describing its main bottleneck, that is, constraint solving.
Then, we survey recent techniques that tackle this bottleneck highlighting their strengths and weaknesses. We continue presenting our original approach, Utopia.
We conclude demonstrating the effectiveness and the efficiency of our approach on four benchmarks of formulas belonging to different logics and in conjunction with a modern symbolic executor of Java bytecode.
The results reported in this thesis confirm that a large portion of the solutions of formulas generated during symbolic program analysis can be reused to efficiently solve other formulas and show that modern symbolic program analysis techniques can largely benefit from solution reuse.

Dissertation Committee:

• Prof. Mauro Pezzè, Università della Svizzera italiana, Switzerland (Research Advisor)
• Prof. Michele Lanza, Università della Svizzera italiana, Switzerland (Internal Member)
• Prof. Cesare Pautasso, Università della Svizzera italiana, Switzerland (Internal Member)
• Prof. Cristian Cadar, Imperial College London, United Kingdom (External Member)
• Prof. Paolo Tonella, Fondazione Bruno Kessler, Trento, Italy (External Member)