Sciweavers

Share
CADE
2010
Springer

A Slice-Based Decision Procedure for Type-Based Partial Orders

9 years 9 months ago
A Slice-Based Decision Procedure for Type-Based Partial Orders
Automated software verification and path-sensitive program analysis require the ability to distinguish executable program paths from those that are infeasible. To achieve this, program paths are encoded symbolically as a conjunction of constraints and submitted to an SMT solver; satisfiable path constraints are then analyzed further. In this paper, we study type-related constraints that arise in path-sensitive analysis of object-oriented programs with forms of multiple inheritance. The dynamic type of a value is critical in determining program branching related to dynamic dispatch, type casting, and explicit type tests. We develop a custom decision procedure for queries in a theory of typebased partial orders and show that the procedure is sound and complete, has low complexity, and is amenable to integration into an SMT framework. We present an empirical evaluation that demonstrates the speed and robustness of our procedure relative to Z3.
Elena Sherman, Brady J. Garvin, Matthew B. Dwyer
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2010
Where CADE
Authors Elena Sherman, Brady J. Garvin, Matthew B. Dwyer
Comments (0)
books