Symbolic execution of transition systems with function summaries

Abstract : Reactive systems can be modeled with various kinds of au-tomata, such as Input Output Symbolic Transition Systems (IOSTS). Symbolic execution (SE) applied to IOSTS allows computing constraints associated to IOSTS path executions (path conditions). In this context, generating test cases amounts to finding numerical input values satisfying such constraints using solvers. This paper explores the case where IOSTS models contain functions which are outside of the scope of such solvers. We propose to use function summaries which are logical formulas built from concrete values describing some representative input/output data tuples of the function. We define algorithmic strategies to solve path conditions including such functions based on techniques using and enriching function summaries. Our method has been implemented within the Diversity tool and has been applied to several examples.
Document type :
Conference papers
Complete list of metadatas

Cited literature [33 references]  Display  Hide  Download

https://hal-cea.archives-ouvertes.fr/cea-01810693
Contributor : Imen Boudhiba <>
Submitted on : Friday, June 8, 2018 - 10:17:51 AM
Last modification on : Thursday, February 7, 2019 - 4:15:55 PM
Long-term archiving on : Sunday, September 9, 2018 - 2:10:54 PM

File

TAP17-Rev-BGLP.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : cea-01810693, version 1

Citation

Imen Boudhiba, Christophe Gaston, Pascale Le Gall, Virgile Prévosto. Symbolic execution of transition systems with function summaries. 11th International Conference on Tests & Proofs, Jul 2017, Marburg, Germany. ⟨cea-01810693⟩

Share

Metrics

Record views

65

Files downloads

194