Many symbolic program analysis techniques rely on SMT solvers to verify properties of programs. Despite the remarkable progress made in the development of such tools, SMT solvers still represent a main bottleneck to the scalability of these techniques. Recent approaches tackle this bottleneck by reusing solutions of formulas that recur during program analysis, thus reducing the number of queries to SMT solvers. Current approaches only reuse solutions across formulas that are equivalent to, contained in or implied by other formulas, as identified through a set of predefined rules, and cannot reuse solutions across formulas that differ in their structure, even if they share some potentially reusable solutions. In this paper, we propose a novel approach that can reuse solutions across formulas that share at least one solution, regardless of their structural resemblance. Our approach exploits a novel heuristic to efficiently identify solutions computed for previously solved formulas and most likely shared by new formulas. The results of an empirical evaluation of our approach on two different logics show that our approach can identify on average more reuse opportunities and is markedly faster than competing approaches.

Aquino, A., Denaro, G., Pezze', M. (2017). Heuristically matching solution spaces of arithmetic formulas to efficiently reuse solutions. In Proceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering, ICSE 2017 (pp.427-437). Institute of Electrical and Electronics Engineers Inc. [10.1109/ICSE.2017.46].

Heuristically matching solution spaces of arithmetic formulas to efficiently reuse solutions

DENARO, GIOVANNI;PEZZE', MAURO
2017

Abstract

Many symbolic program analysis techniques rely on SMT solvers to verify properties of programs. Despite the remarkable progress made in the development of such tools, SMT solvers still represent a main bottleneck to the scalability of these techniques. Recent approaches tackle this bottleneck by reusing solutions of formulas that recur during program analysis, thus reducing the number of queries to SMT solvers. Current approaches only reuse solutions across formulas that are equivalent to, contained in or implied by other formulas, as identified through a set of predefined rules, and cannot reuse solutions across formulas that differ in their structure, even if they share some potentially reusable solutions. In this paper, we propose a novel approach that can reuse solutions across formulas that share at least one solution, regardless of their structural resemblance. Our approach exploits a novel heuristic to efficiently identify solutions computed for previously solved formulas and most likely shared by new formulas. The results of an empirical evaluation of our approach on two different logics show that our approach can identify on average more reuse opportunities and is markedly faster than competing approaches.
paper
SMT-based program analysis; symbolic execution; SMT solvers; solutions reuse
English
IEEE/ACM International Conference on Software Engineering, ICSE 2017 20-28 May
2017
Proceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering, ICSE 2017
9781538638682
2017
427
437
7985682
reserved
Aquino, A., Denaro, G., Pezze', M. (2017). Heuristically matching solution spaces of arithmetic formulas to efficiently reuse solutions. In Proceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering, ICSE 2017 (pp.427-437). Institute of Electrical and Electronics Engineers Inc. [10.1109/ICSE.2017.46].
File in questo prodotto:
File Dimensione Formato  
07985682.pdf

Solo gestori archivio

Tipologia di allegato: Publisher’s Version (Version of Record, VoR)
Dimensione 206.88 kB
Formato Adobe PDF
206.88 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/155092
Citazioni
  • Scopus 9
  • ???jsp.display-item.citation.isi??? 9
Social impact