Leveraging Abstract Interpretation for Efficient Dynamic Symbolic Execution. Alatawi, E., Søndergaard, H., & Miller, T. In Rosu, G., Di Penta, M., & Nguyen, T. N., editors, Proceedings of the 32nd ACM/IEEE International Conference on Automated Software Engineering, pages 619–624, 2017. IEEE Computing Society. ![Leveraging Abstract Interpretation for Efficient Dynamic Symbolic Execution [link]](https://bibbase.org/img/filetypes/link.svg "link")
Paper doi abstract bibtex Dynamic Symbolic Execution (DSE) is a technique to automatically generate test inputs by executing the program simultaneously with concrete and symbolic values. A key challenge in DSE is scalability, as executing all feasible program paths is not possible, owing to the possibly exponential or infinite number of program paths. Loops, in particular those where the number of iterations depends on an input of the program, are a source of path explosion. They cause problems because DSE maintains symbolic values that capture only the data dependencies on symbolic inputs. This ignores control dependencies, including loop dependencies that depend indirectly on the inputs. We propose a method to increase the coverage achieved by DSE in the presence of input-data dependent loops and loop dependent branches. We combine DSE with abstract interpretation to find indirect control dependencies, including loop and branch indirect dependencies. Preliminary results show that this results in better coverage, within considerably less time compared to standard DSE.
@inproceedings{Ala-Son-Mil_ASE17,
author = {Eman Alatawi and
Harald S{\o}ndergaard and
Tim Miller},
title = {Leveraging Abstract Interpretation for Efficient Dynamic
Symbolic Execution},
editor = {G. Rosu and M. {Di Penta} and T. N. Nguyen},
booktitle = {Proceedings of the 32nd ACM/IEEE International Conference on
Automated Software Engineering},
pages = {619--624},
publisher = {IEEE Computing Society},
year = {2017},
doi = {10.1109/ASE.2017.8115672},
url_Paper = {https://minerva-access.unimelb.edu.au/rest/bitstreams/7d0c6934-364c-5596-b09d-d0e55f344c13/retrieve},
abstract = {Dynamic Symbolic Execution (DSE) is a technique to automatically
generate test inputs by executing the program simultaneously
with concrete and symbolic values. A key challenge in DSE is
scalability, as executing all feasible program paths is not
possible, owing to the possibly exponential or infinite number
of program paths. Loops, in particular those where the number
of iterations depends on an input of the program, are a source
of path explosion. They cause problems because DSE maintains
symbolic values that capture only the data dependencies on
symbolic inputs. This ignores control dependencies, including
loop dependencies that depend indirectly on the inputs. We
propose a method to increase the coverage achieved by DSE in
the presence of input-data dependent loops and loop dependent
branches. We combine DSE with abstract interpretation to find
indirect control dependencies, including loop and branch
indirect dependencies. Preliminary results show that this
results in better coverage, within considerably less time
compared to standard DSE.},
keywords = {Symbolic execution, Static analysis, Abstract interpretation},
}
Downloads: 0
{"_id":"P4XqPceGox6ySj6Fu","bibbaseid":"alatawi-sndergaard-miller-leveragingabstractinterpretationforefficientdynamicsymbolicexecution-2017","author_short":["Alatawi, E.","Søndergaard, H.","Miller, T."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Eman"],"propositions":[],"lastnames":["Alatawi"],"suffixes":[]},{"firstnames":["Harald"],"propositions":[],"lastnames":["Søndergaard"],"suffixes":[]},{"firstnames":["Tim"],"propositions":[],"lastnames":["Miller"],"suffixes":[]}],"title":"Leveraging Abstract Interpretation for Efficient Dynamic Symbolic Execution","editor":[{"firstnames":["G."],"propositions":[],"lastnames":["Rosu"],"suffixes":[]},{"firstnames":["M."],"propositions":[],"lastnames":["Di Penta"],"suffixes":[]},{"firstnames":["T.","N."],"propositions":[],"lastnames":["Nguyen"],"suffixes":[]}],"booktitle":"Proceedings of the 32nd ACM/IEEE International Conference on Automated Software Engineering","pages":"619–624","publisher":"IEEE Computing Society","year":"2017","doi":"10.1109/ASE.2017.8115672","url_paper":"https://minerva-access.unimelb.edu.au/rest/bitstreams/7d0c6934-364c-5596-b09d-d0e55f344c13/retrieve","abstract":"Dynamic Symbolic Execution (DSE) is a technique to automatically generate test inputs by executing the program simultaneously with concrete and symbolic values. A key challenge in DSE is scalability, as executing all feasible program paths is not possible, owing to the possibly exponential or infinite number of program paths. Loops, in particular those where the number of iterations depends on an input of the program, are a source of path explosion. They cause problems because DSE maintains symbolic values that capture only the data dependencies on symbolic inputs. This ignores control dependencies, including loop dependencies that depend indirectly on the inputs. We propose a method to increase the coverage achieved by DSE in the presence of input-data dependent loops and loop dependent branches. We combine DSE with abstract interpretation to find indirect control dependencies, including loop and branch indirect dependencies. Preliminary results show that this results in better coverage, within considerably less time compared to standard DSE.","keywords":"Symbolic execution, Static analysis, Abstract interpretation","bibtex":"@inproceedings{Ala-Son-Mil_ASE17,\n author = {Eman Alatawi and \n\t\tHarald S{\\o}ndergaard and\n\t\tTim Miller},\n title = {Leveraging Abstract Interpretation for Efficient Dynamic \n\t\tSymbolic Execution},\n editor = {G. Rosu and M. {Di Penta} and T. N. Nguyen},\n booktitle = {Proceedings of the 32nd ACM/IEEE International Conference on \n\t\tAutomated Software Engineering},\n pages = {619--624},\n publisher = {IEEE Computing Society},\n year = {2017},\n doi = {10.1109/ASE.2017.8115672},\n url_Paper = {https://minerva-access.unimelb.edu.au/rest/bitstreams/7d0c6934-364c-5596-b09d-d0e55f344c13/retrieve},\n abstract = {Dynamic Symbolic Execution (DSE) is a technique to automatically\n\t\tgenerate test inputs by executing the program simultaneously \n\t\twith concrete and symbolic values. A key challenge in DSE is \n\t\tscalability, as executing all feasible program paths is not \n\t\tpossible, owing to the possibly exponential or infinite number \n\t\tof program paths. Loops, in particular those where the number \n\t\tof iterations depends on an input of the program, are a source \n\t\tof path explosion. They cause problems because DSE maintains \n\t\tsymbolic values that capture only the data dependencies on\n\t\tsymbolic inputs. This ignores control dependencies, including \n\t\tloop dependencies that depend indirectly on the inputs. We \n\t\tpropose a method to increase the coverage achieved by DSE in \n\t\tthe presence of input-data dependent loops and loop dependent \n\t\tbranches. We combine DSE with abstract interpretation to find \n\t\tindirect control dependencies, including loop and branch \n\t\tindirect dependencies. Preliminary results show that this \n\t\tresults in better coverage, within considerably less time \n\t\tcompared to standard DSE.},\n keywords = {Symbolic execution, Static analysis, Abstract interpretation},\n}\n\n","author_short":["Alatawi, E.","Søndergaard, H.","Miller, T."],"editor_short":["Rosu, G.","Di Penta, M.","Nguyen, T. N."],"key":"Ala-Son-Mil_ASE17","id":"Ala-Son-Mil_ASE17","bibbaseid":"alatawi-sndergaard-miller-leveragingabstractinterpretationforefficientdynamicsymbolicexecution-2017","role":"author","urls":{" paper":"https://minerva-access.unimelb.edu.au/rest/bitstreams/7d0c6934-364c-5596-b09d-d0e55f344c13/retrieve"},"keyword":["Symbolic execution","Static analysis","Abstract interpretation"],"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/zarajoy/testbibtex/refs/heads/main/test.bib","dataSources":["yWvm3kzg5vKQAPLm7","ofmsZryxNDBSpE7j5","9aC4cxLD8D6oJ3FLN","BNGFBQQncqevukxoe","q5pWX4XZgAS4TQBof","yb3uN577XrYa7qf57","9jmvjAEoFta6emcgS","XqcrNTrCCBr9mSd37","W7ih7WyQivP4EDh83"],"keywords":["symbolic execution","static analysis","abstract interpretation"],"search_terms":["leveraging","abstract","interpretation","efficient","dynamic","symbolic","execution","alatawi","søndergaard","miller"],"title":"Leveraging Abstract Interpretation for Efficient Dynamic Symbolic Execution","year":2017}