Content deleted Content added
→Tools: Add 'Maat' to symbolic execution engines |
Citation bot (talk | contribs) Add: title. Changed bare reference to CS1/2. | Use this bot. Report bugs. | Suggested by BrownHairedGirl | Linked from User:BrownHairedGirl/Articles_with_bare_links | #UCB_webform_linked 1267/2847 |
||
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>{{Cite web|url=https://cacm.acm.org/magazines/2016/6/202649-enhancing-symbolic-execution-with-veritesting/fulltext|title=Enhancing Symbolic Execution with Veritesting}}</ref>
===Program-dependent efficiency===
| |||