Reusing Constraint Proofs in Symbolic Analysis

You are cordially invited to attend the PhD Dissertation Defense of Meixian CHEN on Thursday, May 24 2018 at 13h30 in room A-32 (Red building)

Abstract:

Symbolic analysis is an important element of program verification and automatic testing. Symbolic analysis techniques abstract program properties as expressions of symbolic input values to characterise the program logical constraints, and rely on Satisfiability Modulo Theories (SMT) solvers to both validate the satisfiability of the constraint expression and verify the corresponding program properties.

Despite the impressive improvements of constraint solving and the availability of mature solvers, constraint solving still represents a main bottleneck towards efficient and scalable symbolic program analysis. The work on the SMT bottleneck proceeds along two main research lines: (i) optimisation approaches that assist and complement the solvers in the context of the program analysis in various ways, and (ii) reuse approaches that reduce the invocation of constraint solvers, by reusing proofs while solving constraints during symbolic analysis.

This thesis contributes to the research in reuse approaches, with REusing-Constraint- proofs-in-symbolic-AnaLysis (ReCal), a new approach for reusing proofs across constraints that recur during analysis. ReCal advances over state-of-the-art approaches for reusing constraints by (i) proposing a novel canonical form to efficiently store and retrieve equivalent and related-by-implication constraints, and (ii) defining a parallel framework for GPU-based platforms to optimise the storage and retrieval of constraints and reusable proofs.

Equivalent constraints vary widely due to the program specific details. This thesis defines a canonical form of constraints in the context of symbolic analysis, and develops an original canonicalisation algorithm to generate the canonical form. The canonical form turns the complex problem of deciding the equivalence of two constraints to the simple problem of comparing for equality their canonical forms, thus enabling efficient catching recurring constraints during symbolic analysis.

Constraints can become extremely large when analysing complex systems, and handling large constraints may introduce a heavy overhead, thus harming the scalability of proof-reusing approaches. The ReCal parallel framework largely improves both the performance and scalability of reusing proofs by benefitting from Graphics Processing Units (GPU) platforms that provide thousands of computing units working in parallel. The parallel ReCal framework ReCal-gpu achieves a 10-times speeding up in constraint solving during symbolic execution of various programs.

Dissertation Committee:

• Prof. Mauro Pezzè, Università della Svizzera italiana, Switzerland (Research Advisor)
• Prof. Walter Binder, Università della Svizzera italiana, Switzerland (Internal Member)
• Prof. Mehdi Jazayeri, Università della Svizzera italiana, Switzerland (Internal Member)
• Prof. Andrea De Lucia, Università di Salerno, Italy (External Member)
• Prof. Gordon Fraser, University of Sheffield, UK (External Member)