{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,28]],"date-time":"2026-03-28T16:58:24Z","timestamp":1774717104654,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540272311","type":"print"},{"value":"9783540316862","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11513988_13","type":"book-chapter","created":{"date-parts":[[2010,3,12]],"date-time":"2010-03-12T13:33:28Z","timestamp":1268400808000},"page":"139-143","source":"Crossref","is-referenced-by-count":31,"title":["Saturn: A SAT-Based Tool for Bug Detection"],"prefix":"10.1007","author":[{"given":"Yichen","family":"Xie","sequence":"first","affiliation":[]},{"given":"Alex","family":"Aiken","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","volume-title":"Compilers: Principles, Techniques, and Tools","author":"A.V. Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley, Reading (1986)"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Aiken, A., Foster, J.S., Kodumal, J., Terauchi, T.: Checking and inferring local non-aliasing. In: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, pp. 129\u2013140 (June 2003)","DOI":"10.1145\/781131.781146"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45139-0_7","volume-title":"Model Checking Software","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 103\u2013122. Springer, Heidelberg (2001)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"13_CR5","unstructured":"Das, M., Lerner, S., Seigle, M.: Path-sensitive program verification in polynomial time. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, Berlin, Germany (June 2002)"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Engler, D., Chelf, B., Chou, A., Hallem, S.: Checking system rules using system specific, programmer-written compiler extensions. In: Proceedings of Operating Systems Design and Implementation, OSDI (September 2000)","DOI":"10.21236\/ADA419626"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, pp. 1\u201312 (June 2002)","DOI":"10.1145\/512529.512531"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Hallem, S., Chelf, B., Xie, Y., Engler, D.: A system and language for building system-specific, static analyses. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, Berlin, Germany (June 2002)","DOI":"10.1145\/512529.512539"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Lazy abstraction. In: Proceedings of the 29th Annual Symposium on Principles of Programming Languages, POPL (January 2002)","DOI":"10.1145\/503272.503279"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with Blast. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"key":"13_CR11","unstructured":"Ivancic, F., Yang, Z., Ganai, M., Gupta, A., Ashar, P.: Efficient SAT-based bounded model checking for software verification. In: Proceedings of 1st International Symposium on Leveraging Applications of Formal Methods, ISoLA (2004)"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: Proceedings of the 2000 ACM SIGSOFT International Symposium on Software Testing and Analysis (2000)","DOI":"10.1145\/347324.383378"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Kroening, D., Clarke, E., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: Proceedings of the 40th Design Automation Conference (2003)","DOI":"10.1145\/775925.775928"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"G. Necula","year":"2002","unstructured":"Necula, G., McPeak, S., Rahul, S., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol.\u00a02304, p. 213. Springer, Heidelberg (2002)"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Semeria, L., Micheli, G.D.: SpC: synthesis of pointers in C, application of pointer analysis to the behavioral synthesis from C. In: Proceedings of 21st IEEE\/ACM International Conference on Computer Aided Design, ICCAD (1998)","DOI":"10.1109\/ICCAD.1998.742894"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. In: Proceedings of the 32th Annual Symposium on Principles of Programming Languages, POPL (January 2005)","DOI":"10.1145\/1040305.1040334"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11513988_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:04:59Z","timestamp":1605643499000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11513988_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540272311","9783540316862"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/11513988_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}