TY - GEN
T1 - A slice-based decision procedure for type-based partial orders
AU - Sherman, Elena
AU - Garvin, Brady J.
AU - Dwyer, Matthew B.
PY - 2010
Y1 - 2010
N2 - 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 type-based 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.
AB - 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 type-based 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.
UR - http://www.scopus.com/inward/record.url?scp=77955265276&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-14203-1_14
DO - 10.1007/978-3-642-14203-1_14
M3 - Conference contribution
AN - SCOPUS:77955265276
SN - 3642142028
SN - 9783642142024
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 156
EP - 170
BT - Automated Reasoning - 5th International Joint Conference, IJCAR 2010, Proceedings
T2 - 5th International Joint Conference on Automated Reasoning, IJCAR 2010
Y2 - 16 July 2010 through 19 July 2010
ER -