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].

Reusing constraint proofs in program analysis

DENARO, GIOVANNI
Penultimo
;
PEZZE', MAURO
Ultimo
2015

Abstract

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.
Si
paper
Constraint canonicalization; Constraint solving for symbolic program analysis; Proof reuse; Software
English
International Symposium on Software Testing and Analysis, ISSTA 13-17 july
9781450336208
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].
Aquino, A; Bianchi, F; Chen, M; Denaro, G; Pezze', M
File in questo prodotto:
File Dimensione Formato  
2771783.2771802.pdf

Solo gestori archivio

Tipologia di allegato: Publisher’s Version (Version of Record, VoR)
Dimensione 877.67 kB
Formato Adobe PDF
877.67 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10281/137108
Citazioni
  • Scopus 25
  • ???jsp.display-item.citation.isi??? ND
Social impact