Symbolic Execution with Invariant Inlay: Evaluating the Potential. Alatawi, E., Miller, T., & Søndergaard, H. In Proceedings of the 25th Australasian Software Engineering Conference (ASWEC 2018), pages 26–30, 2018. IEEE Computing Society.
Symbolic Execution with Invariant Inlay: Evaluating the Potential [link]Paper  doi  abstract   bibtex   
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. To capitalise fully on a static analyzer, invariant inlay first applies certain testability transformations to the program source. In this paper we account for how we have evaluated the idea experimentally, in order to determine its usefulness for programs with complex control flow.
@inproceedings{Ala-Mil-Son_ASWEC18,
  author    = {Eman Alatawi and 
		Tim Miller and 
		Harald S{\o}ndergaard},
  title     = {Symbolic Execution with Invariant Inlay:
                Evaluating the Potential},
  booktitle = {Proceedings of the 25th Australasian Software Engineering
                Conference (ASWEC 2018)},
  pages     = {26--30},
  publisher = {IEEE Computing Society},
  year      = {2018},
  doi       = {10.1109/ASWEC.2018.00012},
  url_Paper = {https://minerva-access.unimelb.edu.au/rest/bitstreams/38cf593c-2b7f-5e30-aa42-13b74180ed5d/retrieve},
  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. To capitalise fully on a 
		static analyzer, invariant inlay first applies certain 
		testability transformations to the program source. In this 
		paper we account for how we have evaluated the idea 
		experimentally, in order to determine its usefulness for
		programs with complex control flow.},
  keywords  = {Symbolic execution, Static analysis},
}

Downloads: 0