{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,26]],"date-time":"2026-03-26T03:23:44Z","timestamp":1774495424205,"version":"3.50.1"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2008,12,1]],"date-time":"2008-12-01T00:00:00Z","timestamp":1228089600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCR-0121403"],"award-info":[{"award-number":["CCR-0121403"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["CNS-0238570-001"],"award-info":[{"award-number":["CNS-0238570-001"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000180","name":"U.S. Department of Homeland Security","doi-asserted-by":"publisher","award":["FA8750-05-2-0142"],"award-info":[{"award-number":["FA8750-05-2-0142"]}],"id":[{"id":"10.13039\/100000180","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Inf. Syst. Secur."],"published-print":{"date-parts":[[2008,12]]},"abstract":"<jats:p>\n            This article presents EXE, an effective bug-finding tool that automatically generates inputs that crash real code. Instead of running code on manually or randomly constructed input, EXE runs it on symbolic input initially allowed to be anything. As checked code runs, EXE tracks the constraints on each symbolic (i.e., input-derived) memory location. If a statement uses a symbolic value, EXE does not run it, but instead adds it as an input-constraint; all other statements run as usual. If code conditionally checks a symbolic expression, EXE forks execution, constraining the expression to be true on the true branch and false on the other. Because EXE reasons about all possible values on a path, it has much more power than a traditional runtime tool: (1) it can force execution down any feasible program path and (2) at dangerous operations (e.g., a pointer dereference), it detects if the current path constraints allow\n            <jats:italic>any<\/jats:italic>\n            value that causes a bug. When a path terminates or hits a bug, EXE automatically generates a test case by solving the current path constraints to find concrete values using its own co-designed constraint solver, STP. Because EXE\u2019s constraints have no approximations, feeding this concrete input to an uninstrumented version of the checked code will cause it to follow the same path and hit the same bug (assuming deterministic code).\n          <\/jats:p>\n          <jats:p>EXE works well on real code, finding bugs along with inputs that trigger them in: the BSD and Linux packet filter implementations, the dhcpd DHCP server, the pcre regular expression library, and three Linux file systems.<\/jats:p>","DOI":"10.1145\/1455518.1455522","type":"journal-article","created":{"date-parts":[[2008,12,17]],"date-time":"2008-12-17T13:25:20Z","timestamp":1229520320000},"page":"1-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":261,"title":["EXE"],"prefix":"10.1145","volume":"12","author":[{"given":"Cristian","family":"Cadar","sequence":"first","affiliation":[{"name":"Stanford University"}]},{"given":"Vijay","family":"Ganesh","sequence":"additional","affiliation":[{"name":"Stanford University"}]},{"given":"Peter M.","family":"Pawlowski","sequence":"additional","affiliation":[{"name":"Stanford University"}]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[{"name":"Stanford University"}]},{"given":"Dawson R.","family":"Engler","sequence":"additional","affiliation":[{"name":"Stanford University"}]}],"member":"320","published-online":{"date-parts":[[2008,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11561163_1"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the 18th International Conference on Computer Aided Verification (CAV\u201906)","volume":"4144","author":"Ball T.","unstructured":"Ball , T. and Jones , R. B ., eds. 2006 . Proceedings of the 18th International Conference on Computer Aided Verification (CAV\u201906) , Seattle, WA. Lecture Notes in Computer Science , vol. 4144 . Springer. Ball, T. and Jones, R. B., eds. 2006. Proceedings of the 18th International Conference on Computer Aided Verification (CAV\u201906), Seattle, WA. Lecture Notes in Computer Science, vol. 4144. Springer."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the Workshop on Model Checking of Software (SPIN\u201901)","author":"Ball T.","unstructured":"Ball , T. and Rajamani , S . 2001. Automatically validating temporal safety properties of interfaces . In Proceedings of the Workshop on Model Checking of Software (SPIN\u201901) . Ball, T. and Rajamani, S. 2001. Automatically validating temporal safety properties of interfaces. In Proceedings of the Workshop on Model Checking of Software (SPIN\u201901)."},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 18th International Conference on Computer Aided Verification (CAV\u201904)","author":"Barrett C.","unstructured":"Barrett , C. and Berezin , S . 2004. CVC Lite: A new implementation of the cooperating validity checker . In Proceedings of the 18th International Conference on Computer Aided Verification (CAV\u201904) , R. Alur and D. A. Peled Eds. Lecture Notes in Computer Science. Springer. Barrett, C. and Berezin, S. 2004. CVC Lite: A new implementation of the cooperating validity checker. In Proceedings of the 18th International Conference on Computer Aided Verification (CAV\u201904), R. Alur and D. A. Peled Eds. Lecture Notes in Computer Science. Springer."},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the 2nd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR\u201904)","author":"Barrett C.","unstructured":"Barrett , C. , Berezin , S. , Shikanian , I. , Chechik , M. , Gurfinkel , A. , and Dill , D. L . 2004. A practical approach to partial functions in CVC Lite . In Proceedings of the 2nd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR\u201904) , Cork, Ireland. Barrett, C., Berezin, S., Shikanian, I., Chechik, M., Gurfinkel, A., and Dill, D. L. 2004. A practical approach to partial functions in CVC Lite. In Proceedings of the 2nd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR\u201904), Cork, Ireland."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/390016.808445"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the IEEE International Conference on Automated Software Engineering (ASE\u201900)","author":"Brat G.","unstructured":"Brat , G. , Havelund , K. , Park , S. , and Visser , W . 2000. Model checking programs . In Proceedings of the IEEE International Conference on Automated Software Engineering (ASE\u201900) . Brat, G., Havelund, K., Park, S., and Visser, W. 2000. Model checking programs. In Proceedings of the IEEE International Conference on Automated Software Engineering (ASE\u201900)."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2006.41"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the Conference on Computer-Aided Verification (CAV\u201902)","author":"Bryant R. E.","unstructured":"Bryant , R. E. , Lahiri , S. K. , and Seshia , S. A . 2002. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions . In Proceedings of the Conference on Computer-Aided Verification (CAV\u201902) , E. Brinksma and K. G. Larsen Eds. Springer-Verlag, 78--92. Bryant, R. E., Lahiri, S. K., and Seshia, S. A. 2002. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In Proceedings of the Conference on Computer-Aided Verification (CAV\u201902), E. Brinksma and K. G. Larsen Eds. Springer-Verlag, 78--92."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1097-024X(200006)30:7%3C775::AID-SPE309%3E3.0.CO;2-H"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11537328_2"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180405.1180445"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1119772.1119831"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_30"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337234"},{"key":"e_1_2_1_17_1","unstructured":"Cormen T. H. Leiserson C. E. Rivest R. L. and Stein C. 2001. Introduction to Algorithms. The MIT Electrical Engineering and Computer Science Series. MIT Press\/McGraw Hill. Cormen T. H. Leiserson C. E. Rivest R. L. and Stein C. 2001. Introduction to Algorithms . The MIT Electrical Engineering and Computer Science Series. MIT Press\/McGraw Hill."},{"key":"e_1_2_1_18_1","unstructured":"Coverity. SWAT: the Coverity software analysis toolset. http:\/\/coverity.com. Coverity . SWAT: the Coverity software analysis toolset. http:\/\/coverity.com."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378811"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201903)","author":"Een N.","unstructured":"Een , N. and Sorensson , N . 2003. An extensible SAT-solver . In Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201903) . 78--92. Een, N. and Sorensson, N. 2003. An extensible SAT-solver. In Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201903). 78--92."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/226155.226158"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349328"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512531"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/271771.271790"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/288195.288321"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the Winter USENIX Conference (USENIX\u201992)","author":"Hastings R.","unstructured":"Hastings , R. and Joyce , B . 1992. Purify: Fast detection of memory leaks and access errors . In Proceedings of the Winter USENIX Conference (USENIX\u201992) . Hastings, R. and Joyce, B. 1992. Purify: Fast detection of memory leaks and access errors. In Proceedings of the Winter USENIX Conference (USENIX\u201992)."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/784820.784841"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201903)","author":"Khurshid S.","unstructured":"Khurshid , S. , Pasareanu , C. S. , and Visser , W . 2003. Generalized symbolic execution for model checking and testing . In Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201903) . Khurshid, S., Pasareanu, C. S., and Visser, W. 2003. Generalized symbolic execution for model checking and testing. In Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201903)."},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the 12th USENIX Security Symposium (SECURITY\u201903)","author":"Larson E.","unstructured":"Larson , E. and Austin , T . 2003. High coverage detection of input-related security faults . In Proceedings of the 12th USENIX Security Symposium (SECURITY\u201903) . Larson, E. and Austin, T. 2003. High coverage detection of input-related security faults. In Proceedings of the 12th USENIX Security Symposium (SECURITY\u201903)."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/96267.96279"},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of the International Conference on Compiler Construction (CC\u201902)","author":"Necula G. C.","unstructured":"Necula , G. C. , McPeak , S. , Rahul , S. , and Weimer , W . 2002. CIL: Intermediate language and tools for analysis and transformation of C programs . In Proceedings of the International Conference on Compiler Construction (CC\u201902) . Necula, G. C., McPeak, S., Rahul, S., and Weimer, W. 2002. CIL: Intermediate language and tools for analysis and transformation of C programs. In Proceedings of the International Conference on Compiler Construction (CC\u201902)."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)81040-5"},{"key":"e_1_2_1_39_1","unstructured":"PCRE. PCRE - Perl Compatible Regular Expressions. http:\/\/www.pcre.org\/.  PCRE. PCRE - Perl Compatible Regular Expressions. http:\/\/www.pcre.org\/."},{"key":"e_1_2_1_40_1","volume-title":"CERT","year":"2005","unstructured":"PCRE - CERT 2005 . PCRE Regular Expression Heap Overflow. US-CERT Cyber Security Bulletin SB05-334. http:\/\/www.us-cert.gov\/cas\/bulletins\/SB05-334.html#pcre. PCRE - CERT 2005. PCRE Regular Expression Heap Overflow. US-CERT Cyber Security Bulletin SB05-334. http:\/\/www.us-cert.gov\/cas\/bulletins\/SB05-334.html#pcre."},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of the 11th Annual Network and Distributed System Security Symposium (NDSS\u201904)","author":"Ruwase O.","unstructured":"Ruwase , O. and Lam , M. S . 2004. A practical dynamic buffer overflow detector . In Proceedings of the 11th Annual Network and Distributed System Security Symposium (NDSS\u201904) . 159--169. Ruwase, O. and Lam, M. S. 2004. A practical dynamic buffer overflow detector. In Proceedings of the 11th Annual Network and Distributed System Security Symposium (NDSS\u201904). 159--169."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_2_1_43_1","unstructured":"SMTLIB 2006. SMTLIB competition. http:\/\/www.csl.sri.com\/users\/demoura\/smt-comp.  SMTLIB 2006. SMTLIB competition. http:\/\/www.csl.sri.com\/users\/demoura\/smt-comp."},{"key":"e_1_2_1_44_1","volume-title":"Proceedings of the Network and Distributed Systems Security Conference (NDSS\u201900)","author":"Wagner D.","unstructured":"Wagner , D. , Foster , J. , Brewer , E. , and Aiken , A . 2000. A first step towards automated detection of buffer overrun vulnerabilities . In Proceedings of the Network and Distributed Systems Security Conference (NDSS\u201900) . San Diego, CA. Wagner, D., Foster, J., Brewer, E., and Aiken, A. 2000. A first step towards automated detection of buffer overrun vulnerabilities. In Proceedings of the Network and Distributed Systems Security Conference (NDSS\u201900). San Diego, CA."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040334"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_13"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2006.7"},{"key":"e_1_2_1_48_1","volume-title":"Proceedings of the Symposium on Operating Systems Design and Implementation (OSDI\u201904)","author":"Yang J.","unstructured":"Yang , J. , Twohey , P. , Engler , D. , and Musuvathi , M . 2004. Using model checking to find serious file system errors . In Proceedings of the Symposium on Operating Systems Design and Implementation (OSDI\u201904) . Yang, J., Twohey, P., Engler, D., and Musuvathi, M. 2004. Using model checking to find serious file system errors. In Proceedings of the Symposium on Operating Systems Design and Implementation (OSDI\u201904)."}],"container-title":["ACM Transactions on Information and System Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1455518.1455522","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1455518.1455522","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:18Z","timestamp":1750287258000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1455518.1455522"}},"subtitle":["Automatically Generating Inputs of Death"],"short-title":[],"issued":{"date-parts":[[2008,12]]},"references-count":48,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2008,12]]}},"alternative-id":["10.1145\/1455518.1455522"],"URL":"https:\/\/doi.org\/10.1145\/1455518.1455522","relation":{},"ISSN":["1094-9224","1557-7406"],"issn-type":[{"value":"1094-9224","type":"print"},{"value":"1557-7406","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,12]]},"assertion":[{"value":"2007-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2007-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-12-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}