Symbolic execution systematically explores program paths by solving path conditions --- formulas over symbolic variables. Typically, the symbolic variables range over numbers, arrays and strings. We introduce symbolic execution with existential second-order constraints --- an extension of traditional symbolic execution that allows symbolic variables to range over functions whose interpretations are restricted by a user-defined language. The aims of this new technique are twofold. First, it offers a general analysis framework that can be applied in multiple domains such as program repair and library modelling. Secondly, it addresses the path explosion problem of traditional first-order symbolic execution in certain applications. To realize this technique, we integrate symbolic execution with program synthesis. Specifically, we propose a method of second-order constraint solving that provides efficient proofs of unsatisfiability, which is critical for the performance of symbolic execution. Our evaluation shows that the proposed technique (1) helps to repair programs with loops by mitigating the path explosion, (2) can enable analysis of applications written against unavailable libraries by modelling these libraries from the usage context.

Symbolic execution with existential second-order constraints / Mechtaev, Sergey; Griggio, Alberto; Cimatti, Alessandro; Roychoudhury, Abhik. - (2018), pp. 389-399. (Intervento presentato al convegno 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering tenutosi a Lake Buena Vista, FL, USA nel November 04 - 09, 2018) [10.1145/3236024.3236049].

Symbolic execution with existential second-order constraints

Griggio, Alberto;Cimatti, Alessandro;
2018-01-01

Abstract

Symbolic execution systematically explores program paths by solving path conditions --- formulas over symbolic variables. Typically, the symbolic variables range over numbers, arrays and strings. We introduce symbolic execution with existential second-order constraints --- an extension of traditional symbolic execution that allows symbolic variables to range over functions whose interpretations are restricted by a user-defined language. The aims of this new technique are twofold. First, it offers a general analysis framework that can be applied in multiple domains such as program repair and library modelling. Secondly, it addresses the path explosion problem of traditional first-order symbolic execution in certain applications. To realize this technique, we integrate symbolic execution with program synthesis. Specifically, we propose a method of second-order constraint solving that provides efficient proofs of unsatisfiability, which is critical for the performance of symbolic execution. Our evaluation shows that the proposed technique (1) helps to repair programs with loops by mitigating the path explosion, (2) can enable analysis of applications written against unavailable libraries by modelling these libraries from the usage context.
2018
Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/SIGSOFT FSE 2018
New York
ACM
9781450355735
Mechtaev, Sergey; Griggio, Alberto; Cimatti, Alessandro; Roychoudhury, Abhik
Symbolic execution with existential second-order constraints / Mechtaev, Sergey; Griggio, Alberto; Cimatti, Alessandro; Roychoudhury, Abhik. - (2018), pp. 389-399. (Intervento presentato al convegno 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering tenutosi a Lake Buena Vista, FL, USA nel November 04 - 09, 2018) [10.1145/3236024.3236049].
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/11572/342981
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 27
  • ???jsp.display-item.citation.isi??? ND
social impact