@inproceedings{Lin-Mil-Son_ASWEC15,
  author    = {Yude Lin and 
		Tim Miller and 
		Harald S{\o}ndergaard},
  title     = {Compositional Symbolic Execution Using Fine-Grained Summaries},
  booktitle = {Proceedings of the 24th Australasian Software Engineering
                Conference (ASWEC 2015)},
  pages     = {213--222},
  publisher = {IEEE Computing Society},
  year      = {2015},
  doi       = {10.1109/ASWEC.2015.32},
  url_Paper = {http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=7365810},
  abstract  = {Compositional symbolic execution has been proposed as a way to 
		increase the efficiency of symbolic execution. Essentially, 
		when a function is symbolically executed, a \emph{summary} of 
		the path that was executed is stored. This summary records the 
		precondition and postcondition of the path, and on subsequent 
		calls that satisfy that precondition, the corresponding 
		postcondition can be returned instead of executing the function
		again. However, using functions as the unit of summarisation 
		leaves the symbolic execution tool at the mercy of a program 
		designer, essentially resulting in an arbitrary summarisation 
		strategy. In this paper, we explore the use of 
		\emph{fine-grained} summaries, in which blocks \emph{within} 
		functions are summarised. We propose three types of 
		summarisation and demonstrate how to generate these. At such a 
		fine-grained level, symbolic execution of a path effectively 
		becomes the concatenation of the summaries along that path. 
		Using a prototype symbolic execution tool, we perform a 
		preliminary experimental evaluation of our summary approaches, 
		demonstrating that they can improve the speed of symbolic 
		execution by reducing the number of calls sent to the 
		underlying constraint solver.},
  keywords  = {Symbolic execution},
}

{"_id":"5fo4tcm7vLcKnPYgP","bibbaseid":"lin-miller-sndergaard-compositionalsymbolicexecutionusingfinegrainedsummaries-2015","author_short":["Lin, Y.","Miller, T.","Søndergaard, H."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Yude"],"propositions":[],"lastnames":["Lin"],"suffixes":[]},{"firstnames":["Tim"],"propositions":[],"lastnames":["Miller"],"suffixes":[]},{"firstnames":["Harald"],"propositions":[],"lastnames":["Søndergaard"],"suffixes":[]}],"title":"Compositional Symbolic Execution Using Fine-Grained Summaries","booktitle":"Proceedings of the 24th Australasian Software Engineering Conference (ASWEC 2015)","pages":"213–222","publisher":"IEEE Computing Society","year":"2015","doi":"10.1109/ASWEC.2015.32","url_paper":"http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=7365810","abstract":"Compositional symbolic execution has been proposed as a way to increase the efficiency of symbolic execution. Essentially, when a function is symbolically executed, a \\emphsummary of the path that was executed is stored. This summary records the precondition and postcondition of the path, and on subsequent calls that satisfy that precondition, the corresponding postcondition can be returned instead of executing the function again. However, using functions as the unit of summarisation leaves the symbolic execution tool at the mercy of a program designer, essentially resulting in an arbitrary summarisation strategy. In this paper, we explore the use of \\emphfine-grained summaries, in which blocks \\emphwithin functions are summarised. We propose three types of summarisation and demonstrate how to generate these. At such a fine-grained level, symbolic execution of a path effectively becomes the concatenation of the summaries along that path. Using a prototype symbolic execution tool, we perform a preliminary experimental evaluation of our summary approaches, demonstrating that they can improve the speed of symbolic execution by reducing the number of calls sent to the underlying constraint solver.","keywords":"Symbolic execution","bibtex":"@inproceedings{Lin-Mil-Son_ASWEC15,\n author = {Yude Lin and \n\t\tTim Miller and \n\t\tHarald S{\\o}ndergaard},\n title = {Compositional Symbolic Execution Using Fine-Grained Summaries},\n booktitle = {Proceedings of the 24th Australasian Software Engineering\n Conference (ASWEC 2015)},\n pages = {213--222},\n publisher = {IEEE Computing Society},\n year = {2015},\n doi = {10.1109/ASWEC.2015.32},\n url_Paper = {http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=7365810},\n abstract = {Compositional symbolic execution has been proposed as a way to \n\t\tincrease the efficiency of symbolic execution. Essentially, \n\t\twhen a function is symbolically executed, a \\emph{summary} of \n\t\tthe path that was executed is stored. This summary records the \n\t\tprecondition and postcondition of the path, and on subsequent \n\t\tcalls that satisfy that precondition, the corresponding \n\t\tpostcondition can be returned instead of executing the function\n\t\tagain. However, using functions as the unit of summarisation \n\t\tleaves the symbolic execution tool at the mercy of a program \n\t\tdesigner, essentially resulting in an arbitrary summarisation \n\t\tstrategy. In this paper, we explore the use of \n\t\t\\emph{fine-grained} summaries, in which blocks \\emph{within} \n\t\tfunctions are summarised. We propose three types of \n\t\tsummarisation and demonstrate how to generate these. At such a \n\t\tfine-grained level, symbolic execution of a path effectively \n\t\tbecomes the concatenation of the summaries along that path. \n\t\tUsing a prototype symbolic execution tool, we perform a \n\t\tpreliminary experimental evaluation of our summary approaches, \n\t\tdemonstrating that they can improve the speed of symbolic \n\t\texecution by reducing the number of calls sent to the \n\t\tunderlying constraint solver.},\n keywords = {Symbolic execution},\n}\n\n","author_short":["Lin, Y.","Miller, T.","Søndergaard, H."],"key":"Lin-Mil-Son_ASWEC15","id":"Lin-Mil-Son_ASWEC15","bibbaseid":"lin-miller-sndergaard-compositionalsymbolicexecutionusingfinegrainedsummaries-2015","role":"author","urls":{" paper":"http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=7365810"},"keyword":["Symbolic execution"],"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/zarajoy/testbibtex/refs/heads/main/test.bib","dataSources":["yWvm3kzg5vKQAPLm7","ofmsZryxNDBSpE7j5","9aC4cxLD8D6oJ3FLN","wpkuJrZJJtqra3FbL","W7ih7WyQivP4EDh83","BNGFBQQncqevukxoe","q5pWX4XZgAS4TQBof","yb3uN577XrYa7qf57","9jmvjAEoFta6emcgS","XqcrNTrCCBr9mSd37"],"keywords":["symbolic execution"],"search_terms":["compositional","symbolic","execution","using","fine","grained","summaries","lin","miller","søndergaard"],"title":"Compositional Symbolic Execution Using Fine-Grained Summaries","year":2015}