{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T18:52:09Z","timestamp":1777488729094,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":33,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2006,7,21]]},"DOI":"10.1145\/1146238.1146251","type":"proceedings-article","created":{"date-parts":[[2006,7,24]],"date-time":"2006-07-24T16:53:01Z","timestamp":1153759981000},"page":"109-120","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":74,"title":["Modular verification of code with SAT"],"prefix":"10.1145","author":[{"given":"Greg","family":"Dennis","sequence":"first","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA"}]},{"given":"Felix Sheng-Ho","family":"Chang","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA"}]},{"given":"Daniel","family":"Jackson","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA"}]}],"member":"320","published-online":{"date-parts":[[2006,7,21]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"6\n   .170 Laboratory in Software Engineering Fall 2001. http:\/\/www.ocw.mit.edu\/OcwWeb\/Electrical- Engineering-and-Computer-Science\/6-170Fall- 2005\/CourseHome\/.]]  6.170 Laboratory in Software Engineering Fall 2001. http:\/\/www.ocw.mit.edu\/OcwWeb\/Electrical- Engineering-and-Computer-Science\/6-170Fall- 2005\/CourseHome\/.]]"},{"key":"e_1_3_2_1_2_1","unstructured":"GNU Trove: High performance collections for Java. http:\/\/trove4j.sourceforge.net\/.]]  GNU Trove: High performance collections for Java. http:\/\/trove4j.sourceforge.net\/.]]"},{"key":"e_1_3_2_1_3_1","unstructured":"Jakarta Commons-Collections. http:\/\/jakarta.apache.org\/commons\/collections\/.]]  Jakarta Commons-Collections. http:\/\/jakarta.apache.org\/commons\/collections\/.]]"},{"key":"e_1_3_2_1_4_1","unstructured":"JML Specifications for the Java Collections Framework. http:\/\/www.cs.iastate.edu\/leavens\/JMLrelease\/javadocs\/java\/util\/Collection.html.]]  JML Specifications for the Java Collections Framework. http:\/\/www.cs.iastate.edu\/leavens\/JMLrelease\/javadocs\/java\/util\/Collection.html.]]"},{"key":"e_1_3_2_1_5_1","unstructured":"The Alloy Analyzer. http:\/\/alloy.mit.edu\/.]]  The Alloy Analyzer. http:\/\/alloy.mit.edu\/.]]"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/646483.691738"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566191"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/2932433.2932497"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_3_2_1_12_1","first-page":"385","volume-title":"Modular Verification of Software Components in C. In ICSE '03: Proceedings of the 25th International Conference on Software Engineering","author":"Chaki S.","year":"2003","unstructured":"S. Chaki , E. Clarke , A. Groce , S. Jha , and H. Veith . Modular Verification of Software Components in C. In ICSE '03: Proceedings of the 25th International Conference on Software Engineering , pages 385 -- 395 , Washington, DC, USA , 2003 .]] S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith. Modular Verification of Software Components in C. In ICSE '03: Proceedings of the 25th International Conference on Software Engineering, pages 385--395, Washington, DC, USA, 2003.]]"},{"key":"e_1_3_2_1_13_1","volume-title":"NuSMV: A New Symbolic Model Verifier. In 11th International Conference on Computer Aided Verification (CAV'99)","author":"Cimatti A.","year":"2003","unstructured":"A. Cimatti , E. Clarke , F. Giunchiglia , and M. Roveri . NuSMV: A New Symbolic Model Verifier. In 11th International Conference on Computer Aided Verification (CAV'99) , Trento, Italy, pages 495- -499, July , 2003 .]] A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: A New Symbolic Model Verifier. In 11th International Conference on Computer Aided Verification (CAV'99), Trento, Italy, pages 495--499, July, 2003.]]"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/355045.355063"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503219"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/347324.383378"},{"key":"e_1_3_2_1_20_1","volume-title":"Essays on Programming Methodology","author":"Jackson D.","year":"2000","unstructured":"D. Jackson . Object Models as Heap Invariants . In Essays on Programming Methodology , edited by Carroll Morgan and Annabelle McIver. Springer Verlag , 2000 .]] D. Jackson. Object Models as Heap Invariants. In Essays on Programming Methodology, edited by Carroll Morgan and Annabelle McIver. Springer Verlag, 2000.]]"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_22_1","series-title":"Lecture Notes in Computer Science","first-page":"59","volume-title":"Computer Systems: Papers for Roger Needham","author":"Lampson B. W.","year":"2004","unstructured":"B. W. Lampson . Software Components: Only the Giants Survive . In K. S. J. Andrew Herbert, editor, Computer Systems: Papers for Roger Needham , Lecture Notes in Computer Science , pages 59 -- 65 . Springer-Verlag Berlin , 2004 .]] B. W. Lampson. Software Components: Only the Giants Survive. In K. S. J. Andrew Herbert, editor, Computer Systems: Papers for Roger Needham, Lecture Notes in Computer Science, pages 59--65. Springer-Verlag Berlin, 2004.]]"},{"key":"e_1_3_2_1_23_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/978-3-540-45099-3_15","volume-title":"SAS 2000: Static Analysis, 7th International Symposium","author":"Lev-Ami T.","year":"2000","unstructured":"T. Lev-Ami and M. Sagiv . TVLA: A System for Implementing Static Analyses . In SAS 2000: Static Analysis, 7th International Symposium , Santa Barbara, CA, USA , volume 1824 of Lecture Notes in Computer Science , pages 280 -- 302 , 2000 .]] T. Lev-Ami and M. Sagiv. TVLA: A System for Implementing Static Analyses. In SAS 2000: Static Analysis, 7th International Symposium, Santa Barbara, CA, USA, volume 1824 of Lecture Notes in Computer Science, pages 280--302, 2000.]]"},{"key":"e_1_3_2_1_24_1","first-page":"22","volume-title":"TestEra: A Novel Framework for Automated Testing of Java Programs. In ASE '2001: 16th IEEE International Conference on Automated Software Engineering","author":"Marinov D.","year":"2001","unstructured":"D. Marinov and S. Khurshid . TestEra: A Novel Framework for Automated Testing of Java Programs. In ASE '2001: 16th IEEE International Conference on Automated Software Engineering , pages 22 -- 31 , 2001 .]] D. Marinov and S. Khurshid. TestEra: A Novel Framework for Automated Testing of Java Programs. In ASE '2001: 16th IEEE International Conference on Automated Software Engineering, pages 22--31, 2001.]]"},{"key":"e_1_3_2_1_25_1","first-page":"88","volume-title":"Software Engineering Concepts and Techniques (1968 NATO Conference of Software Engineering)","author":"McIlroy M. D.","year":"1968","unstructured":"M. D. McIlroy . Mass-Produced Software Components. In J. M. Buxton, P. Naur, and B. Randell, editors , Software Engineering Concepts and Techniques (1968 NATO Conference of Software Engineering) , pages 88 -- 98 . NATO Science Committee , Oct 1968 .]] M. D. McIlroy. Mass-Produced Software Components. In J. M. Buxton, P. Naur, and B. Randell, editors, Software Engineering Concepts and Techniques (1968 NATO Conference of Software Engineering), pages 88--98. NATO Science Committee, Oct 1968.]]"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"McMillan K. L.","year":"1993","unstructured":"K. L. McMillan . Symbolic Model Checking . Kluwer Academic Publishers , 1993 .]] K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.]]"},{"key":"e_1_3_2_1_27_1","unstructured":"Sun Microsystems. Java Collections Framework. http:\/\/java.sun.com\/j2se\/1.5.0\/docs\/guide\/collections\/.]]  Sun Microsystems. Java Collections Framework. http:\/\/java.sun.com\/j2se\/1.5.0\/docs\/guide\/collections\/.]]"},{"key":"e_1_3_2_1_28_1","volume-title":"Detect Errors in Code. In ASE '2004: 19th IEEE International Conference on Automated Software Engineering","author":"Taghdiri M.","year":"2004","unstructured":"M. Taghdiri . Inferring Specifications to Detect Errors in Code. In ASE '2004: 19th IEEE International Conference on Automated Software Engineering , Linz, Austria, pages 144--153 , 2004 .]] M. Taghdiri. Inferring Specifications to Detect Errors in Code. In ASE '2004: 19th IEEE International Conference on Automated Software Engineering, Linz, Austria, pages 144--153, 2004.]]"},{"key":"e_1_3_2_1_29_1","volume-title":"The Design of a Relational Engine. Submitted for publication","author":"Torlak E.","year":"2006","unstructured":"E. Torlak and D. Jackson . The Design of a Relational Engine. Submitted for publication , 2006 .]] E. Torlak and D. Jackson. The Design of a Relational Engine. Submitted for publication, 2006.]]"},{"key":"e_1_3_2_1_30_1","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson D.","year":"2006","unstructured":"D. Jackson . Software Abstractions: Logic, Language, and Analysis . MIT Press , Cambridge, MA , 2006 .]] D. Jackson. Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge, MA, 2006.]]"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/646485.694447"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765920"},{"key":"e_1_3_2_1_34_1","first-page":"3","volume-title":"Model Checking Programs. In ASE '2000: 15th IEEE International Conference on Automated Software Engineering","author":"Visser W.","year":"2000","unstructured":"W. Visser , K. Havelund , G. Brat , and S. Park . Model Checking Programs. In ASE '2000: 15th IEEE International Conference on Automated Software Engineering , pages 3 -- 11 , 2000 .]] W. Visser, K. Havelund, G. Brat, and S. Park. Model Checking Programs. In ASE '2000: 15th IEEE International Conference on Automated Software Engineering, pages 3--11, 2000.]]"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_13"}],"event":{"name":"ISSTA06: International Symposium on Software Testing and Analysis 2006","location":"Portland Maine USA","acronym":"ISSTA06","sponsor":["ACM Association for Computing Machinery","SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 2006 international symposium on Software testing and analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1146238.1146251","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,12]],"date-time":"2023-01-12T08:28:40Z","timestamp":1673512120000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1146238.1146251"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,7,21]]},"references-count":33,"alternative-id":["10.1145\/1146238.1146251","10.1145\/1146238"],"URL":"https:\/\/doi.org\/10.1145\/1146238.1146251","relation":{},"subject":[],"published":{"date-parts":[[2006,7,21]]},"assertion":[{"value":"2006-07-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}