In this paper we propose an approach for reusing formula solutions to reduce the impact of Satisfiability Modulo Theories (SMT) solvers on the scalability of symbolic program analysis. SMT solvers can efficiently handle huge expressions in relevant logic theories, but they still represent a main bottleneck to the scalability of symbolic analyses, like symbolic execution and symbolic model checking. Reusing proofs of formulas solved during former analysis sessions can reduce the amount of invocations of SMT solvers, thus mitigating the impact of SMT solvers on symbolic program analysis. Early approaches to reuse formula solutions exploit equivalence and inclusion relations among structurally similar formulas, and are strongly tighten to the specific target logics. In this paper, we present an original approach that reuses both satisfiability and unsatisfiability proofs shared among many formulas beyond only equivalent or related-by-implication formulas. Our approach straightforwardly generalises across multiple logics. It is based on the original concept of distance between formulas, which heuristically approximates the likelihood of formulas to share either satisfiability or unsatisfiability proofs. We show the efficiency and the generalisability of our approach, by instantiating the underlying distance function for formulas that belong to most popular logic theories handled by current SMT solvers, and confirm the effectiveness of the approach, by reporting experimental results on over nine millions formulas from five logic theories.

Aquino, A., Denaro, G., Pezze, M. (2021). Reusing Solutions Modulo Theories. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 47(5), 948-968 [10.1109/TSE.2019.2898199].

Reusing Solutions Modulo Theories

Denaro, G;Pezze, M
2021

Abstract

In this paper we propose an approach for reusing formula solutions to reduce the impact of Satisfiability Modulo Theories (SMT) solvers on the scalability of symbolic program analysis. SMT solvers can efficiently handle huge expressions in relevant logic theories, but they still represent a main bottleneck to the scalability of symbolic analyses, like symbolic execution and symbolic model checking. Reusing proofs of formulas solved during former analysis sessions can reduce the amount of invocations of SMT solvers, thus mitigating the impact of SMT solvers on symbolic program analysis. Early approaches to reuse formula solutions exploit equivalence and inclusion relations among structurally similar formulas, and are strongly tighten to the specific target logics. In this paper, we present an original approach that reuses both satisfiability and unsatisfiability proofs shared among many formulas beyond only equivalent or related-by-implication formulas. Our approach straightforwardly generalises across multiple logics. It is based on the original concept of distance between formulas, which heuristically approximates the likelihood of formulas to share either satisfiability or unsatisfiability proofs. We show the efficiency and the generalisability of our approach, by instantiating the underlying distance function for formulas that belong to most popular logic theories handled by current SMT solvers, and confirm the effectiveness of the approach, by reporting experimental results on over nine millions formulas from five logic theories.
Articolo in rivista - Articolo scientifico
SMT solver; solution reuse; symbolic execution; Symbolic program analysis;
English
4-apr-2019
2021
47
5
948
968
8681653
none
Aquino, A., Denaro, G., Pezze, M. (2021). Reusing Solutions Modulo Theories. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 47(5), 948-968 [10.1109/TSE.2019.2898199].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/228173
Citazioni
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 1
Social impact