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. 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
{"_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}