{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:18:06Z","timestamp":1770283086833,"version":"3.49.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"3","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2007,5]]},"abstract":"<jats:p>This article presents Saturn, a general framework for building precise and scalable static error detection systems. Saturn exploits recent advances in Boolean satisfiability (SAT) solvers and is path sensitive, precise down to the bit level, and models pointers and heap data. Our approach is also highly scalable, which we achieve using two techniques. First, for each program function, several optimizations compress the size of the Boolean formulas that model the control flow and data flow and the heap locations accessed by a function. Second, summaries in the spirit of type signatures are computed for each function, allowing interprocedural analysis without a dramatic increase in the size of the Boolean constraints to be solved.<\/jats:p>\n          <jats:p>We have experimentally validated our approach by conducting two case studies involving a Linux lock checker and a memory leak checker. Results from the experiments show that our system scales well, parallelizes well, and finds more errors with fewer false positives than previous static error detection systems.<\/jats:p>","DOI":"10.1145\/1232420.1232423","type":"journal-article","created":{"date-parts":[[2007,6,6]],"date-time":"2007-06-06T14:37:11Z","timestamp":1181140631000},"page":"16","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":98,"title":["Saturn"],"prefix":"10.1145","volume":"29","author":[{"given":"Yichen","family":"Xie","sequence":"first","affiliation":[{"name":"Stanford University, Stanford, CA"}]},{"given":"Alex","family":"Aiken","sequence":"additional","affiliation":[{"name":"Stanford University, Stanford, CA"}]}],"member":"320","published-online":{"date-parts":[[2007,5]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1177220"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781146"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of Fourth International Conference on Integrated Formal Methods. Springer","author":"Ball T."},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the SPIN 2001 Workshop on Model Checking of Software. Lecture Notes in Computer Science","volume":"2057","author":"Ball T."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_6_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_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1024393.1024412"},{"key":"e_1_2_1_8_1","unstructured":"Chou A. 2003. Static analysis for bug finding in systems software. Ph.D. dissertation. Stanford University Stanford CA.   Chou A. 2003. Static analysis for bug finding in systems software. Ph.D. dissertation. Stanford University Stanford CA."},{"key":"e_1_2_1_9_1","volume-title":"Eds. Lecture Notes in Computer Science","volume":"2988","author":"Clarke E."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000040025.89719.f3"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/178243.178264"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the Conference on Operating Systems Design and Implementation (OSDI).","author":"Engler D."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/231379.231389"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512531"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Hackett B. and Aiken A. 2005. How is aliasing used in systems software&quest; Tech. rep. Stanford University Stanford CA.  Hackett B. and Aiken A. 2005. How is aliasing used in systems software&quest; Tech. rep. Stanford University Stanford CA.","DOI":"10.1145\/1181775.1181785"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040331"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512539"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the Winter USENIX Conference.","author":"Hastings R."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781150"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the SPIN 2003 Workshop on Model Checking Software. Lecture Notes in Computer Science","volume":"2648","author":"Henzinger T. A."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/347324.383378"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer","author":"Khurshid S."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775928"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/143095.143137"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 8th Static Analysis Symposium.","author":"Liang D."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349327"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/320384.320400"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/207110.207111"},{"key":"e_1_2_1_32_1","unstructured":"Xie Y. and Chou A. 2002. Path sensitive analysis using Boolean satisfiability. Tech. rep. Stanford University Stanford CA.  Xie Y. and Chou A. 2002. Path sensitive analysis using Boolean satisfiability. Tech. rep. Stanford University Stanford CA."},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the International Conference on Computer-Aided Design","author":"Zhang L."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1232420.1232423","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T19:06:22Z","timestamp":1672254382000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1232420.1232423"}},"subtitle":["A scalable framework for error detection using Boolean satisfiability"],"short-title":[],"issued":{"date-parts":[[2007,5]]},"references-count":33,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2007,5]]}},"alternative-id":["10.1145\/1232420.1232423"],"URL":"https:\/\/doi.org\/10.1145\/1232420.1232423","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,5]]},"assertion":[{"value":"2007-05-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}