Symbolic execution of transition systems with function summaries

Imen Boudhiba; Christophe Gaston; Pascale Le Gall; Virgile Prevosto

doi:10.1007/978-3-319-61467-0_3

Symbolic execution of transition systems with function summaries

Imen Boudhiba, Christophe Gaston, Pascale Le Gall, Virgile Prevosto

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Tests and Proofs - 11th International Conference, TAP 2017 Held as Part of STAF 2017, Proceedings
Editors	Einar Broch Johnsen, Sebastian Gabmeyer
Publisher	Springer Verlag
Pages	41-58
Number of pages	18
ISBN (Print)	9783319614663
DOIs	https://doi.org/10.1007/978-3-319-61467-0_3
Publication status	Published - 1 Jan 2017
Externally published	Yes
Event	11th International Conference on Tests and Proofs, TAP 2017, held as part of STAF 2017 - Marburg, Germany Duration: 19 Jul 2017 → 20 Jul 2017

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10375 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	11th International Conference on Tests and Proofs, TAP 2017, held as part of STAF 2017
Country/Territory	Germany
City	Marburg
Period	19/07/17 → 20/07/17

Keywords

Functions summaries
Input output symbolic transition systems
Symbolic execution
Transition coverage

Access to Document

10.1007/978-3-319-61467-0_3

Cite this

Boudhiba, I., Gaston, C., Le Gall, P., & Prevosto, V. (2017). Symbolic execution of transition systems with function summaries. In E. B. Johnsen, & S. Gabmeyer (Eds.), Tests and Proofs - 11th International Conference, TAP 2017 Held as Part of STAF 2017, Proceedings (pp. 41-58). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10375 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-61467-0_3

Boudhiba, Imen ; Gaston, Christophe ; Le Gall, Pascale et al. / Symbolic execution of transition systems with function summaries. Tests and Proofs - 11th International Conference, TAP 2017 Held as Part of STAF 2017, Proceedings. editor / Einar Broch Johnsen ; Sebastian Gabmeyer. Springer Verlag, 2017. pp. 41-58 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@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",

}

Boudhiba, I, Gaston, C, Le Gall, P & Prevosto, V 2017, Symbolic execution of transition systems with function summaries. in EB Johnsen & S Gabmeyer (eds), Tests and Proofs - 11th International Conference, TAP 2017 Held as Part of STAF 2017, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10375 LNCS, Springer Verlag, pp. 41-58, 11th International Conference on Tests and Proofs, TAP 2017, held as part of STAF 2017, Marburg, Germany, 19/07/17. https://doi.org/10.1007/978-3-319-61467-0_3

Symbolic execution of transition systems with function summaries. / Boudhiba, Imen; Gaston, Christophe; Le Gall, Pascale et al.
Tests and Proofs - 11th International Conference, TAP 2017 Held as Part of STAF 2017, Proceedings. ed. / Einar Broch Johnsen; Sebastian Gabmeyer. Springer Verlag, 2017. p. 41-58 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10375 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Symbolic execution of transition systems with function summaries

AU - Boudhiba, Imen

AU - Gaston, Christophe

AU - Le Gall, Pascale

AU - Prevosto, Virgile

N1 - Publisher Copyright: © Springer International Publishing AG 2017.

PY - 2017/1/1

Y1 - 2017/1/1

N2 - 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.

AB - 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.

KW - Functions summaries

KW - Input output symbolic transition systems

KW - Symbolic execution

KW - Transition coverage

U2 - 10.1007/978-3-319-61467-0_3

DO - 10.1007/978-3-319-61467-0_3

M3 - Conference contribution

AN - SCOPUS:85025123530

SN - 9783319614663

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 41

EP - 58

BT - Tests and Proofs - 11th International Conference, TAP 2017 Held as Part of STAF 2017, Proceedings

A2 - Johnsen, Einar Broch

A2 - Gabmeyer, Sebastian

PB - Springer Verlag

T2 - 11th International Conference on Tests and Proofs, TAP 2017, held as part of STAF 2017

Y2 - 19 July 2017 through 20 July 2017

ER -

Boudhiba I, Gaston C, Le Gall P, Prevosto V. Symbolic execution of transition systems with function summaries. In Johnsen EB, Gabmeyer S, editors, Tests and Proofs - 11th International Conference, TAP 2017 Held as Part of STAF 2017, Proceedings. Springer Verlag. 2017. p. 41-58. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-61467-0_3

Symbolic execution of transition systems with function summaries

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this