@inproceedings{243f9635a06842a6a2f7c304debc6e32,
title = "Symbolic execution of transition systems with function summaries",
abstract = "Reactive systems can be modeled with various kinds of automata, 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.",
keywords = "Functions summaries, Input output symbolic transition systems, Symbolic execution, Transition coverage",
author = "Imen Boudhiba and Christophe Gaston and \{Le Gall\}, Pascale and Virgile Prevosto",
note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2017.; 11th International Conference on Tests and Proofs, TAP 2017, held as part of STAF 2017 ; Conference date: 19-07-2017 Through 20-07-2017",
year = "2017",
month = jan,
day = "1",
doi = "10.1007/978-3-319-61467-0\_3",
language = "English",
isbn = "9783319614663",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "41--58",
editor = "Johnsen, \{Einar Broch\} and Sebastian Gabmeyer",
booktitle = "Tests and Proofs - 11th International Conference, TAP 2017 Held as Part of STAF 2017, Proceedings",
}