Powered by OpenAIRE graph
Found an issue? Give us feedback
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/ HAL-Pasteur; HAL-Ins...arrow_drop_down
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO; Lecture Notes in Computer Science
Other literature type . Part of book or chapter of book . Conference object . 2017 . 2018 . Peer-reviewed
License: Springer TDM
versions View all 17 versions
addClaim

This Research product is the result of merged Research products in OpenAIRE.

You have already added 0 works in your ORCID record related to the merged Research product.

Symbolic Execution of Transition Systems with Function Summaries

Authors: Boudhiba, Imen; Gaston, Christophe; Gall, Pascale Le; Prevosto, Virgile;

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.

Conference of 11th International Conference on Tests and Proofs, TAP 2017, held as part of STAF 2017 ; Conference Date: 19 July 2017 Through 20 July 2017; Conference Code:194199

International audience

Country
France
Subjects by Vocabulary

Microsoft Academic Graph classification: Model checking Theoretical computer science Computer science Symbolic execution Input/output Function (mathematics) Test case Path (graph theory) Transition system Tuple

Keywords

Artificial intelligence, Model checking, Functions summaries, [ INFO ] Computer Science [cs], Transition system, Transition coverage, Numerical inputs, [INFO]Computer Science [cs], Input/output datum, Logical formulas, Symbolic Transition Systems, Function summaries, Computers, Computer science, Symbolic Execution, Input Output Symbolic Transition Systems, Functions sum- maries

36 references, page 1 of 4

1. Saswat Anand, Patrice Godefroid, and Nikolai Tillmann. Demand-driven compositional symbolic execution. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 367{381, Berlin, Heidelberg, 2008. Springer-Verlag.

2. Saswat Anand, Corina S. Pasareanu, and Willem Visser. Jpf-se: A symbolic execution extension to java path nder. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 134{138, Berlin, Heidelberg, 2007. Springer-Verlag.

3. Mathilde Arnaud, Boutheina Bannour, and Arnault Lapitre. An illustrative use case of the diversity platform based on uml interaction scenarios. Electron. Notes Theor. Comput. Sci., pages 21{34, 2016. [OpenAIRE]

4. Domagoj Babic and Alan J. Hu. Structural abstraction of software veri cation conditions. In Proceedings of the 19th International Conference on Computer Aided Veri cation, pages 366{378, Berlin, Heidelberg, 2007. Springer-Verlag.

5. Boutheina Bannour, Jose Pablo Escobedo, Christophe Gaston, and Pascale Le Gall. O -line test case generation for timed symbolic model-based conformance testing. In Testing Software and Systems, pages 119{135. Springer, 2012.

6. Boutheina Bannour, Christophe Gaston, Marc Aiguier, and Arnault Lapitre. Results for compositional timed testing. In 20th Asia-Paci c Software Engineering Conference, APSEC, pages 559{564. IEEE Computer Society, 2013.

7. N. Bj rner, N. Tillmann, and A. Voronkov. Path feasibility analysis for stringmanipulating programs. In TACAS, volume 5505 of LNCS. Springer, 2009.

8. Imen Boudhiba, Christophe Gaston, Pascale Le Gall, and Virgile Prevosto. Modelbased testing from input output symbolic transition systems enriched by program calls and contracts. In Testing Software and Systems - 27th IFIP WG 6.1 International Conference, ICTSS, volume 9447 of Lecture Notes in Computer Science, pages 35{51. Springer, 2015.

9. Cristian Cadar and Dawson Engler. Execution generated test cases: How to make systems code crash itself. Software Model Checking (SPIN), 2005. [OpenAIRE]

10. James C.King. Symbolic execution and program testing. Communication ACM, 19:385{394, 1976.

  • BIP!
    Impact byBIP!
    citations
    This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    0
    popularity
    This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
    Average
    influence
    This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    Average
    impulse
    This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
    Average
    OpenAIRE UsageCounts
    Usage byUsageCounts
    visibility views 100
    download downloads 151
  • citations
    This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    0
    popularity
    This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
    Average
    influence
    This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    Average
    impulse
    This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
    Average
    Powered byBIP!BIP!
  • 100
    views
    151
    downloads
    Powered byOpenAIRE UsageCounts
Powered by OpenAIRE graph
Found an issue? Give us feedback
visibility
download
citations
This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Citations provided by BIP!
popularity
This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
BIP!Popularity provided by BIP!
influence
This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Influence provided by BIP!
impulse
This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
BIP!Impulse provided by BIP!
views
OpenAIRE UsageCountsViews provided by UsageCounts
downloads
OpenAIRE UsageCountsDownloads provided by UsageCounts
0
Average
Average
Average
100
151