{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:12:01Z","timestamp":1784844721689,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540712084","type":"print"},{"value":"9783540712091","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71209-1_49","type":"book-chapter","created":{"date-parts":[[2007,7,4]],"date-time":"2007-07-04T22:56:34Z","timestamp":1183589794000},"page":"632-647","source":"Crossref","is-referenced-by-count":271,"title":["Kodkod: A Relational Model Finder"],"prefix":"10.1007","author":[{"given":"Emina","family":"Torlak","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniel","family":"Jackson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"49_CR1","doi-asserted-by":"crossref","unstructured":"Jackson, D., Shlyakhter, I., Sridharan, M.: A micromodularity mechanism. In: ESEC\/SIGSOFT FSE, pp. 62\u201373 (2001)","DOI":"10.1145\/503209.503219"},{"key":"49_CR2","series-title":"Lecture Notes in Computer Science","first-page":"505","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Jackson","year":"2003","unstructured":"Jackson, D., Vaziri, M.: Checking Properties of Heap-Manipulating Procedures with a Constraint Solver. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol.\u00a02619, pp. 505\u2013520. Springer, Heidelberg (2003)"},{"key":"49_CR3","doi-asserted-by":"crossref","unstructured":"Taghdiri, M.: Inferring specifications to detect errors in code. In: ASE, pp. 144\u2013153 (2004)","DOI":"10.1109\/ASE.2004.1342732"},{"issue":"4","key":"49_CR4","first-page":"403","volume":"11","author":"S. Khurshid","year":"2004","unstructured":"Khurshid, S., Marinov, D.: TestEra: Specification-based testing of java programs using sat. ASE\u00a011(4), 403\u2013434 (2004)","journal-title":"ASE"},{"key":"49_CR5","doi-asserted-by":"crossref","unstructured":"Dennis, G., Chang, F., Jackson, D.: Modular verification of code. In: ISSTA, Portland, Maine (2006)","DOI":"10.1145\/1146238.1146251"},{"key":"49_CR6","unstructured":"Yeung, V.: Declarative configuration applied to course scheduling. Master\u2019s thesis, Massachusetts Institute of Technology, Cambridge, MA (2006)"},{"key":"49_CR7","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve MACE-style finite model finding. In: CADE-19 Workshop on Model Computation, Miami, FL (2003)"},{"key":"49_CR8","unstructured":"McCune, W.: A Davis-Putnam program and its application to finite first-order model search: quasigroup existence problem. Technical report, ANL (1994)"},{"issue":"2","key":"49_CR9","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"49_CR10","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1145\/1007512.1007544","volume-title":"ISSTA \u201904","author":"J. Edwards","year":"2004","unstructured":"Edwards, J., et al.: Faster constraint solving with subtypes. In: ISSTA \u201904, pp. 232\u2013242. ACM Press, New York (2004)"},{"key":"49_CR11","doi-asserted-by":"crossref","unstructured":"Andersen, H.R., Hulgaard, H.: Boolean expression diagrams. In: LICS, Warsaw, Poland (1997)","DOI":"10.1109\/LICS.1997.614938"},{"key":"49_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/3-540-46419-0_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"2000","unstructured":"Abdulla, P.A., Bjesse, P., E\u00e9n, N.: Symbolic reachability analysis based on sat-solvers. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol.\u00a01785, pp. 411\u2013425. Springer, Heidelberg (2000)"},{"key":"49_CR13","unstructured":"Torlak, E., Dennis, G.: Kodkod for Alloy users. In: First ACM Alloy Workshop, Portland, Oregon (2006)"},{"key":"49_CR14","unstructured":"Fujita, M., Slaney, J., Bennett, F.: Automating generation of some results in finite algebra. In: 13th IJCAI, Chamb\u00e9ry, France (1993)"},{"key":"49_CR15","doi-asserted-by":"crossref","unstructured":"Jackson, D.: Automating first order relational logic. In: FSE, San Diego, CA (2000)","DOI":"10.1145\/355045.355063"},{"issue":"2","key":"49_CR16","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1145\/276393.276396","volume":"20","author":"D. Jackson","year":"1998","unstructured":"Jackson, D., Jha, S., Damon, C.A.: Isomorph-free model enumeration: a new method for checking relational specifications. ACM TPLS\u00a020(2), 302\u2013343 (1998)","journal-title":"ACM TPLS"},{"key":"49_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"798","DOI":"10.1007\/3-540-58156-1_63","volume-title":"Automated Deduction - CADE-12","author":"J.K. Slaney","year":"1994","unstructured":"Slaney, J.K.: Finder: Finite domain enumerator - system description. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814, pp. 798\u2013801. Springer, Heidelberg (1994)"},{"key":"49_CR18","unstructured":"Zhang, J.: The generation and application of finite models. PhD thesis, Institute of Software, Academia Sinica, Beijing (1994)"},{"key":"49_CR19","unstructured":"Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: IJCAI95, Montreal (1995)"},{"key":"49_CR20","doi-asserted-by":"crossref","unstructured":"Jackson, D., Damon, C.A.: Elements of style: analyzing a software design feature with a counterexample detector. TOSEM, 484\u2013495 (1996)","DOI":"10.1145\/229000.226322"},{"key":"49_CR21","unstructured":"Ng, Y.C.: A Nitpick specification of IPv6. Senior Honors thesis, Computer Science Department, Carnegie Mellon University (1997)"},{"key":"49_CR22","doi-asserted-by":"crossref","unstructured":"Khurshid, S., Jackson, D.: Exploring the design of an intentional naming scheme with an automatic constraint analyzer. In: ASE, pp. 13\u201322 (2000)","DOI":"10.1109\/ASE.2000.873646"},{"key":"49_CR23","doi-asserted-by":"crossref","unstructured":"Dennis, G., et al.: Automating commutativity analysis at the design level. In: ISSTA, pp. 165\u2013174 (2004)","DOI":"10.1145\/1007512.1007535"},{"key":"49_CR24","unstructured":"Narain, S.: Network configuration management via model finding. In: ACM Workshop On Self-Managed Systems, Newport Beach, CA (2004)"},{"key":"49_CR25","volume-title":"The Craft of Prolog. Logic Programming","author":"R. O\u2019Keefe","year":"1990","unstructured":"O\u2019Keefe, R.: The Craft of Prolog. Logic Programming. MIT Press, Cambridge (1990)"},{"key":"49_CR26","volume-title":"Concepts, Techniques, and Models of Computer Programming","author":"P. Roy Van","year":"2004","unstructured":"Van Roy, P., Haridi, S.: Concepts, Techniques, and Models of Computer Programming. MIT Press, Cambridge (2004)"},{"key":"49_CR27","first-page":"148","volume-title":"KR\u201996","author":"J. Crawford","year":"1996","unstructured":"Crawford, J., et al.: Symmetry-breaking predicates for search problems. In: KR\u201996, pp. 148\u2013159. Morgan Kaufmann, San Francisco (1996)"},{"key":"49_CR28","doi-asserted-by":"crossref","unstructured":"Shlyakhter, I.: Generating effective symmetry breaking predicates for search problems. Electronic Notes in Discrete Mathematics\u00a09 (2001)","DOI":"10.1016\/S1571-0653(04)00311-7"},{"key":"49_CR29","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-boolean constraints into SAT. In: SBMC, vol.\u00a02, pp. 1\u201326 (2006)","DOI":"10.3233\/SAT190014"},{"key":"49_CR30","series-title":"Lecture Notes in Computer Science","first-page":"360","volume-title":"Theory and Applications of Satisfiability Testing","author":"S. Malik","year":"2005","unstructured":"Malik, S., Fu, Z., Mahajan, Y.S.: Zchaff2004: An Efficient SAT Solver. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 360\u2013375. Springer, Heidelberg (2005)"},{"key":"49_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"49_CR32","unstructured":"Shlyakhter, I.: Declarative Symbolic Pure Logic Model Checking. PhD thesis, Massachusetts Institute of Technology, Cambridge, MA (2005)"},{"key":"49_CR33","unstructured":"Sabharwal, A.: SymChaff: A structure-aware satisfiability solver. In: 20th National Conference on Artificial Intelligence (AAAI), Pittsburgh, PA, Pittsburgh, PA, pp. 467\u2013474 (2005)"},{"key":"49_CR34","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-4034-9","volume-title":"Groups and Symmetry","author":"M.A. Armstrong","year":"1988","unstructured":"Armstrong, M.A.: Groups and Symmetry. Springer, New York (1988)"},{"key":"49_CR35","unstructured":"Torlak, E., Jackson, D.: The design of a relational engine. Technical Report MIT-CSAIL-TR-2006-068, MIT (2006)"},{"key":"49_CR36","first-page":"162","volume-title":"IEEE SFCS","author":"L. Babai","year":"1983","unstructured":"Babai, L., Kantor, W.M., Luks, E.M.: Computational complexity and the classification of finite simple groups. In: IEEE SFCS, pp. 162\u2013171. IEEE CSP, Los Alamitos (1983)"},{"key":"49_CR37","unstructured":"Shlyakhter, I., et al.: Exploiting subformula sharing in automatic analysis of quantified formulas. In: SAT, Portofino, Italy (2003)"},{"key":"49_CR38","first-page":"43","volume-title":"Programming Languages","author":"E.W. Dijkstra","year":"1968","unstructured":"Dijkstra, E.W.: Cooperating sequential processes. In: Genuys, F. (ed.) Programming Languages, pp. 43\u2013112. Academic Press, New York (1968)"},{"issue":"5","key":"49_CR39","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1145\/359104.359108","volume":"22","author":"E.J.H. Chang","year":"1979","unstructured":"Chang, E.J.H., Roberts, R.: An improved algorithm for decentralized extrema-finding in circular configurations of processes. Commun. ACM\u00a022(5), 281\u2013283 (1979)","journal-title":"Commun. ACM"},{"key":"49_CR40","unstructured":"Ramananandro, T.: The Mondex case study with Alloy (2006), http:\/\/www.eleves.ens.fr\/home\/ramanana\/work\/mondex\/"},{"key":"49_CR41","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: A fast and robust SAT solver. In: Design Automation and Test in Europe, pp. 142\u2013149 (2002)","DOI":"10.1109\/DATE.2002.998262"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71209-1_49.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:16:54Z","timestamp":1605763014000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71209-1_49"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540712084","9783540712091"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71209-1_49","relation":{},"subject":[]}}