Symbolic execution: Difference between revisions

Revision as of 14:19, 20 December 2021

Revision as of 05:11, 30 December 2021

Line 26:

===Path explosion===

Symbolically executing all feasible program paths does not scale to large programs. The number of feasible paths in a program grows exponentially with an increase in program size and can even be infinite in the case of programs with unbounded loop iterations.<ref>{{cite book|last=Anand|first=Saswat|author2=Patrice Godefroid |author3=Nikolai Tillmann |chapter=Demand-Driven Compositional Symbolic Execution|title=Tools and Algorithms for the Construction and Analysis of Systems|year=2008|volume=4963|pages=367–381|doi=10.1007/978-3-540-78800-3_28|series=Lecture Notes in Computer Science|isbn=978-3-540-78799-0}}</ref> Solutions to the ''path explosion'' problem generally use either heuristics for path-finding to increase code coverage,<ref>{{cite book|last=Ma|first=Kin-Keng|author2=Khoo Yit Phang |author3=Jeffrey S. Foster |author4=Michael Hicks |chapter=Directed Symbolic Execution|title=Proceedings of the 18th International Conference on Statis Analysis|year=2011|pages=95–111|chapter-url=http://dl.acm.org/citation.cfm?id=2041563|accessdate=2013-04-03|isbn=9783642237010}}</ref> reduce execution time by parallelizing independent paths,<ref>{{cite book|last=Staats|first=Matt|author2=Corina Pasareanu |s2cid=9898522|chapter=Parallel symbolic execution for structural test generation|title=Proceedings of the 19th International Symposium on Software Testing and Analysis|year=2010|pages=183–194|doi=10.1145/1831708.1831732|isbn=9781605588230}}</ref> or by merging similar paths.<ref>{{Cite book|chapter= Efficient State Merging in Symbolic Execution|publisher = ACM|title= Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation|date = 2012-01-01|___location = New York, NY, USA|isbn = 978-1-4503-1205-9|pages = 193–204|series =<!---->|doi = 10.1145/2254064.2254088|first1 = Volodymyr|last1 = Kuznetsov|first2 = Johannes|last2 = Kinder|first3 = Stefan|last3 = Bucur|first4 = George|last4 = Candea|s2cid = 135107|citeseerx = 10.1.1.348.823}}</ref>. One example of merging is ''veritesting'', which "employs static symbolic execution to amplify the effect of dynamic symbolic execution".<ref>https://cacm.acm.org/magazines/2016/6/202649-enhancing-symbolic-execution-with-veritesting/fulltext</ref>.

===Program-dependent efficiency===