Symbolic analysis techniques have largely improved over the years, and are now approaching an industrial maturity level. One of the main limitations to the scalability of symbolic analysis is the impact of constraint solving that is still a relevant bottleneck for the applicability of symbolic techniques, despite the dramatic improvements of the last decades. In this paper we discuss a novel approach to deal with the constraint solving bottleneck. Starting from the observation that constraints may recur during the analysis of the same as well as different programs, we investigate the advantages of complementing constraint solving with searching for the satisfiability proof of a constraint in a repository of constraint proofs. We extend recent proposals with powerful simplifications and an original canonical form of the constraints that reduce syntactically different albeit equivalent constraints to the same form, and thus facilitate the search for equivalent constraints in large repositories. The experimental results we attained indicate that the proposed approach improves over both similar solutions and state of the art constraint solvers.
Aquino, A., Bianchi, F., Chen, M., Denaro, G., & Pezze', M. (2015). Reusing constraint proofs in program analysis. In 2015 International Symposium on Software Testing and Analysis, ISSTA 2015 - Proceedings (pp.305-315). Association for Computing Machinery, Inc [10.1145/2771783.2771802].
|Citazione:||Aquino, A., Bianchi, F., Chen, M., Denaro, G., & Pezze', M. (2015). Reusing constraint proofs in program analysis. In 2015 International Symposium on Software Testing and Analysis, ISSTA 2015 - Proceedings (pp.305-315). Association for Computing Machinery, Inc [10.1145/2771783.2771802].|
|Carattere della pubblicazione:||Scientifica|
|Presenza di un coautore afferente ad Istituzioni straniere:||Si|
|Titolo:||Reusing constraint proofs in program analysis|
|Autori:||Aquino, A; Bianchi, F; Chen, M; Denaro, G; Pezze', M|
DENARO, GIOVANNI (Penultimo)
PEZZE', MAURO (Ultimo)
|Data di pubblicazione:||2015|
|Nome del convegno:||International Symposium on Software Testing and Analysis, ISSTA 13-17 july|
|Digital Object Identifier (DOI):||http://dx.doi.org/10.1145/2771783.2771802|
|Appare nelle tipologie:||02 - Intervento a convegno|