Paper Info
Title
Specification of concretization and symbolization policies in symbolic execution.
Abstract
Symbolic Execution (SE) is a popular and profitable approach to automatic code-based software testing. Concretization and symbolization (C/S) is a crucial part of modern SE tools, since it directly impacts the trade-offs between correctness, completeness and efficiency of the approach. Yet, C/S policies have been barely studied. We intend to remedy to this situation and to establish C/S policies on a firm ground. To this end, we propose a clear separation of concerns between C/S specification on one side, through the new rule-based description language CSml, and the algorithmic core of SE on the other side, revisited to take C/S policies into account. This view is implemented on top of an existing SE tool, demonstrating the feasibility and the benefits of the method. This work paves the way for more flexible SE tools with well-documented and reusable C/S policies, as well as for a systematic study of C/S policies.
Year
DOI
Venue
2016
10.1145/2931037.2931048
ISSTA
Field
DocType
Citations 
Specification language,Programming language,Software engineering,Automatic test generation,Computer science,Correctness,Separation of concerns,Symbolic execution,Formal methods,Completeness (statistics),Software testing
Conference
4
PageRank 
References 
Authors
0.40
21
7
Name
Order
Citations
PageRank
Robin David1422.59
Sébastien Bardin229719.35
Josselin Feist3864.79
Laurent Mounier4118779.54
Marie-Laure Potet519021.34
Thanh Dinh Ta6181.30
Jean-yves Marion764759.49