Title
Symbolic Execution with Invariant Inlay: Evaluating the Potential
Abstract
Dynamic symbolic execution (DSE) is a non-standard execution mechanism which, loosely, executes a program symbolically and, simultaneously, on concrete input. DSE is attractive because of several uses in software engineering, including the generation of test data suites with large coverage relative to test suite size. However, DSE struggles in the face of execution path explosion, and is often unable to cover certain kinds of difficult-to-reach program points. Invariant inlay is a technique that aims to improve a DSE tool by interspersing code with invariants, generated automatically using off-the-shelf tools for static program analysis using abstract interpretation. To capitalise fully on a static analyzer, invariant inlay applies certain instrumentations and testability transformations to the program source. In this paper we outline the invariant inlay approach, and how we have evaluated the idea, in order to determine its usefulness for programs with complex control flow.
Year
DOI
Venue
2018
10.1109/ASWEC.2018.00012
2018 25th Australasian Software Engineering Conference (ASWEC)
Keywords
Field
DocType
symbolic execution,invariant inlay,DSE,Dynamic symbolic execution,abstract interpretation,testability transformations,execution path explosion
Testability,Test suite,Static program analysis,Programming language,Abstract interpretation,Computer science,Control flow,Test data,Symbolic execution,Invariant (mathematics)
Conference
ISSN
ISBN
Citations 
1530-0803
978-1-7281-1242-8
0
PageRank 
References 
Authors
0.34
10
3
Name
Order
Citations
PageRank
Eman Alatawi161.82
Tim Miller214213.81
Harald Søndergaard385879.52