{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:44:38Z","timestamp":1772163878572,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2004,7,1]],"date-time":"2004-07-01T00:00:00Z","timestamp":1088640000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2004,7]]},"DOI":"10.1145\/1007512.1007544","type":"proceedings-article","created":{"date-parts":[[2004,7,20]],"date-time":"2004-07-20T11:55:38Z","timestamp":1090324538000},"page":"232-242","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Faster constraint solving with subtypes"],"prefix":"10.1145","author":[{"given":"Jonathan","family":"Edwards","sequence":"first","affiliation":[{"name":"MIT, Cambridge, MA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Jackson","sequence":"additional","affiliation":[{"name":"MIT, Cambridge, MA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emina","family":"Torlak","sequence":"additional","affiliation":[{"name":"MIT, Cambridge, MA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vincent","family":"Yeung","sequence":"additional","affiliation":[{"name":"MIT, Cambridge, MA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2004,7]]},"reference":[{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/646483.691738"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(96)00047-1"},{"key":"e_1_3_2_1_4_1","volume-title":"Model Checking","author":"Clarke E.","year":"1999","unstructured":"E. Clarke , O. Grumberg , and D. Peled . Model Checking . The MIT Press , 1999 .]] E. Clarke, O. Grumberg, and D. Peled. Model Checking. The MIT Press, 1999.]]"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050046"},{"key":"e_1_3_2_1_6_1","unstructured":"Jonathan Edwards Daniel Jackson and Emina Torlak. A Type System for Object Models. Submitted for publication. http:\/\/sdg.lcs.mit.edu\/pubs\/TR\/typesforobjectmodels.pdf]]  Jonathan Edwards Daniel Jackson and Emina Torlak. A Type System for Object Models. Submitted for publication. http:\/\/sdg.lcs.mit.edu\/pubs\/TR\/typesforobjectmodels.pdf]]"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292543"},{"key":"e_1_3_2_1_8_1","volume-title":"Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI)","author":"Ernst Michael","year":"1997","unstructured":"Michael Ernst , Todd Millstein and Daniel Weld . Automatic SAT compilation of planning problems . Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI) , 1997 .]] Michael Ernst, Todd Millstein and Daniel Weld. Automatic SAT compilation of planning problems. Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI), 1997.]]"},{"key":"e_1_3_2_1_9_1","volume-title":"BerkMin: A Fast and Robust SAT Solver. Design Automation and Test in Europe (DATE)","author":"Goldberg E.","year":"2002","unstructured":"E. Goldberg and Y. Novikov . BerkMin: A Fast and Robust SAT Solver. Design Automation and Test in Europe (DATE) 2002 .]] E. Goldberg and Y. Novikov. BerkMin: A Fast and Robust SAT Solver. Design Automation and Test in Europe (DATE) 2002.]]"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","DOI":"10.1090\/dol\/012","volume-title":"Problems for Mathematicians, Young and Old","author":"Halmos Paul","year":"1991","unstructured":"Paul Halmos . Problems for Mathematicians, Young and Old . The Mathematical Association of America , 1991 .]] Paul Halmos. Problems for Mathematicians, Young and Old. The Mathematical Association of America, 1991.]]"},{"key":"e_1_3_2_1_11_1","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"Holzmann Gerard J.","year":"2004","unstructured":"Gerard J. Holzmann . The SPIN Model Checker: Primer and Reference Manual . Addison-Wesley Professional , 2004 .]] Gerard J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 2004.]]"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/355045.355063"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/276393.276396"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503219"},{"key":"e_1_3_2_1_15_1","unstructured":"Rajeev Joshi Greg Nelson and Keith Randall. Denali: a goal-directed superoptimizer. http:\/\/citeseer.nj.nec.com\/joshi01denali.html]]  Rajeev Joshi Greg Nelson and Keith Randall. Denali: a goal-directed superoptimizer. http:\/\/citeseer.nj.nec.com\/joshi01denali.html]]"},{"key":"e_1_3_2_1_16_1","volume-title":"Proc. European Conference on Artificial Intelligence","author":"Kautz H.","year":"1992","unstructured":"H. Kautz , and B. Selman . Planning as satisfiability . Proc. European Conference on Artificial Intelligence , Vienna, Austria , 1992 .]] H. Kautz, and B. Selman. Planning as satisfiability. Proc. European Conference on Artificial Intelligence, Vienna, Austria, 1992.]]"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/786768.786968"},{"key":"e_1_3_2_1_18_1","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport . Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley Professional , 2002 .]] Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Professional, 2002.]]"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319317"},{"key":"e_1_3_2_1_20_1","volume-title":"Proceedings Formal Methods Europe","author":"Michael","year":"2003","unstructured":"Michael Leuschel and Michael Butler. ProB: A Model Checker for B . Proceedings Formal Methods Europe , 2003 .]] Michael Leuschel and Michael Butler. ProB: A Model Checker for B. Proceedings Formal Methods Europe, 2003.]]"},{"key":"e_1_3_2_1_21_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_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268954"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/253228.253351"},{"key":"e_1_3_2_1_25_1","unstructured":"Piza The Prolog Z Animator. http:\/\/www.noodles.demon.co.uk\/PiZA\/PiZAHome.html]]  Piza The Prolog Z Animator. http:\/\/www.noodles.demon.co.uk\/PiZA\/PiZAHome.html]]"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0653(04)00311-7"},{"key":"e_1_3_2_1_27_1","volume-title":"Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Vaziri Mandana","year":"2003","unstructured":"Mandana Vaziri and Daniel Jackson . Checking Properties of Heap-Manipulating Procedures using a Constraint Solver . Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems , Warsaw, Poland , April , 2003 .]] Mandana Vaziri and Daniel Jackson. Checking Properties of Heap-Manipulating Procedures using a Constraint Solver. Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Warsaw, Poland, April, 2003.]]"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1609\/aimag.v20i2.1459"}],"event":{"name":"ISSTA04: International Symposium on Software Testing and Analysis 2004","location":"Boston Massachusetts USA","acronym":"ISSTA04","sponsor":["ACM Association for Computing Machinery","SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1007512.1007544","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1007512.1007544","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:23:56Z","timestamp":1750253036000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1007512.1007544"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,7]]},"references-count":27,"alternative-id":["10.1145\/1007512.1007544","10.1145\/1007512"],"URL":"https:\/\/doi.org\/10.1145\/1007512.1007544","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1013886.1007544","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2004,7]]},"assertion":[{"value":"2004-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}