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

{"_id":"rgkpoCTunspAWksrJ","bibbaseid":"alatawi-miller-sndergaard-symbolicexecutionwithinvariantinlayevaluatingthepotential-2018","author_short":["Alatawi, E.","Miller, T.","Søndergaard, H."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Eman"],"propositions":[],"lastnames":["Alatawi"],"suffixes":[]},{"firstnames":["Tim"],"propositions":[],"lastnames":["Miller"],"suffixes":[]},{"firstnames":["Harald"],"propositions":[],"lastnames":["Søndergaard"],"suffixes":[]}],"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","bibtex":"@inproceedings{Ala-Mil-Son_ASWEC18,\n author = {Eman Alatawi and \n\t\tTim Miller and \n\t\tHarald S{\\o}ndergaard},\n title = {Symbolic Execution with Invariant Inlay:\n Evaluating the Potential},\n booktitle = {Proceedings of the 25th Australasian Software Engineering\n Conference (ASWEC 2018)},\n pages = {26--30},\n publisher = {IEEE Computing Society},\n year = {2018},\n doi = {10.1109/ASWEC.2018.00012},\n url_Paper = {https://minerva-access.unimelb.edu.au/rest/bitstreams/38cf593c-2b7f-5e30-aa42-13b74180ed5d/retrieve},\n abstract = {Dynamic symbolic execution (DSE) is a non-standard execution \n\t\tmechanism which, loosely, executes a program symbolically and, \n\t\tsimultaneously, on concrete input. DSE is attractive because of\n\t\tseveral uses in software engineering, including the generation\n\t\tof test data suites with large coverage relative to test suite\n\t\tsize. However, DSE struggles in the face of execution path \n\t\texplosion, and is often unable to cover certain kinds of \n\t\tdifficult-to-reach program points. Invariant inlay is a \n\t\ttechnique that aims to improve a DSE tool by interspersing code\n\t\twith invariants, generated automatically using off-the-shelf \n\t\ttools for static program analysis. To capitalise fully on a \n\t\tstatic analyzer, invariant inlay first applies certain \n\t\ttestability transformations to the program source. In this \n\t\tpaper we account for how we have evaluated the idea \n\t\texperimentally, in order to determine its usefulness for\n\t\tprograms with complex control flow.},\n keywords = {Symbolic execution, Static analysis},\n}\n\n","author_short":["Alatawi, E.","Miller, T.","Søndergaard, H."],"key":"Ala-Mil-Son_ASWEC18","id":"Ala-Mil-Son_ASWEC18","bibbaseid":"alatawi-miller-sndergaard-symbolicexecutionwithinvariantinlayevaluatingthepotential-2018","role":"author","urls":{" paper":"https://minerva-access.unimelb.edu.au/rest/bitstreams/38cf593c-2b7f-5e30-aa42-13b74180ed5d/retrieve"},"keyword":["Symbolic execution","Static analysis"],"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"people.eng.unimelb.edu.au/harald/bibbase.bib","dataSources":["yWvm3kzg5vKQAPLm7","ofmsZryxNDBSpE7j5","9aC4cxLD8D6oJ3FLN","XqcrNTrCCBr9mSd37","W7ih7WyQivP4EDh83"],"keywords":["symbolic execution","static analysis"],"search_terms":["symbolic","execution","invariant","inlay","evaluating","potential","alatawi","miller","søndergaard"],"title":"Symbolic Execution with Invariant Inlay: Evaluating the Potential","year":2018}