{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:44:44Z","timestamp":1772163884632,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","license":[{"start":{"date-parts":[[2005,9,1]],"date-time":"2005-09-01T00:00:00Z","timestamp":1125532800000},"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":[[2005,9]]},"DOI":"10.1145\/1081706.1081740","type":"proceedings-article","created":{"date-parts":[[2005,11,7]],"date-time":"2005-11-07T12:34:39Z","timestamp":1131366879000},"page":"207-216","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Relational analysis of algebraic datatypes"],"prefix":"10.1145","author":[{"given":"Viktor","family":"Kuncak","sequence":"first","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Jackson","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2005,9]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"The Alloy project. http:\/\/alloy.mit.edu\/.]]  The Alloy project. http:\/\/alloy.mit.edu\/.]]"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00368-1"},{"key":"e_1_3_2_1_3_1","volume-title":"Introduction to Functional Programming using Haskell","author":"Bird R.","year":"1998","unstructured":"R. Bird . Introduction to Functional Programming using Haskell . Prentice-Hall, Inc. , 2nd edition, 1998 .]] R. Bird. Introduction to Functional Programming using Haskell. Prentice-Hall, Inc., 2nd edition, 1998.]]"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00206-6"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566191"},{"key":"e_1_3_2_1_6_1","first-page":"495","volume-title":"Proceedings Eleventh Conference on Computer-Aided Verification (CAV'99), number 1633 in LNCS","author":"Cimatti A.","year":"1999","unstructured":"A. Cimatti , E. Clarke , F. Giunchiglia , and M. Roveri . NuSMV: a new Symbolic Model Verifier . In N. Halbwachs and D. Peled, editors, Proceedings Eleventh Conference on Computer-Aided Verification (CAV'99), number 1633 in LNCS , pages 495 -- 499 , Trento, Italy, July 1999 . Springer .]] A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: a new Symbolic Model Verifier. In N. Halbwachs and D. Peled, editors, Proceedings Eleventh Conference on Computer-Aided Verification (CAV'99), number 1633 in LNCS, pages 495--499, Trento, Italy, July 1999. Springer.]]"},{"key":"e_1_3_2_1_7_1","volume-title":"Model Computation","author":"Claessen K.","year":"2003","unstructured":"K. Claessen and N. S\u00f6rensson . New techniques that improve MACE-style model finding . In Model Computation , 2003 .]] K. Claessen and N. S\u00f6rensson. New techniques that improve MACE-style model finding. In Model Computation, 2003.]]"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(90)90080-L"},{"key":"e_1_3_2_1_9_1","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0062837","volume-title":"The Computational Complexity of Logical Theories","author":"Ferrante J.","year":"1979","unstructured":"J. Ferrante and C. W. Rackoff . The Computational Complexity of Logical Theories , volume 718 of Lecture Notes in Mathematics . Springer-Verlag , 1979 .]] J. Ferrante and C. W. Rackoff. The Computational Complexity of Logical Theories, volume 718 of Lecture Notes in Mathematics. Springer-Verlag, 1979.]]"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-005-0089-y"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/944331.944360"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359666"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/648237.753964"},{"key":"e_1_3_2_1_14_1","series-title":"Encyclopedia of Mathematics and its Applications","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511551574","volume-title":"Model Theory","author":"Hodges W.","year":"1993","unstructured":"W. Hodges . Model Theory , volume 42 of Encyclopedia of Mathematics and its Applications . Cambridge University Press , 1993 .]] W. Hodges. Model Theory, volume 42 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1993.]]"},{"key":"e_1_3_2_1_15_1","first-page":"636","volume-title":"International Conference on Principles of Knowledge Representation and Reasoning","author":"Horrocks I.","year":"1998","unstructured":"I. Horrocks . Using an expressive description logic: FaCT or fiction ? In International Conference on Principles of Knowledge Representation and Reasoning , pages 636 -- 647 , 1998 .]] I. Horrocks. Using an expressive description logic: FaCT or fiction? In International Conference on Principles of Knowledge Representation and Reasoning, pages 636--647, 1998.]]"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30124-0_15"},{"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","volume-title":"Collected Papers of IFIP Working Group 2.3 on Programming Methodology","author":"Jackson D.","year":"2001","unstructured":"D. Jackson . Object models as heap invariants . In A. McIver and C. Morgan, editors, Collected Papers of IFIP Working Group 2.3 on Programming Methodology . Springer-Verlag , 2001 .]] D. Jackson. Object models as heap invariants. In A. McIver and C. Morgan, editors, Collected Papers of IFIP Working Group 2.3 on Programming Methodology. Springer-Verlag, 2001.]]"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503219"},{"key":"e_1_3_2_1_20_1","first-page":"1","volume-title":"Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science","author":"Burch J.R.","year":"1990","unstructured":"J.R. Burch , E.M. Clarke , K.L. McMillan , D.L. Dill , and L.J. Hwang . Symbolic Model Checking: 1020 States and Beyond . In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science , pages 1 -- 33 , Washington, D.C. , 1990 . IEEE Computer Society Press.]] J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic Model Checking: 1020 States and Beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 1--33, Washington, D.C., 1990. IEEE Computer Society Press.]]"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/647267.760182"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/788023.789075"},{"key":"e_1_3_2_1_25_1","volume-title":"July","author":"Leroy X.","year":"2004","unstructured":"X. Leroy . The Objective Caml system, release 3.08 , July 2004 .]] X. Leroy. The Objective Caml system, release 3.08, July 2004.]]"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/647169.718161"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5132"},{"key":"e_1_3_2_1_29_1","series-title":"Studies in Logic and The Foundations of Mathematics","volume-title":"The Metamathematics of Algebraic Systems","author":"Mal\u0107ev A. I.","year":"1971","unstructured":"A. I. Mal\u0107ev . The Metamathematics of Algebraic Systems , volume 66 of Studies in Logic and The Foundations of Mathematics . North Holland , 1971 .]] A. I. Mal\u0107ev. The Metamathematics of Algebraic Systems, volume 66 of Studies in Logic and The Foundations of Mathematics. North Holland, 1971.]]"},{"key":"e_1_3_2_1_30_1","volume-title":"MIT","author":"Marinov D.","year":"2005","unstructured":"D. Marinov . Automatic Testing of Software with Structurally Complex Inputs. PhD thesis , MIT , 2005 .]] D. Marinov. Automatic Testing of Software with Structurally Complex Inputs. PhD thesis, MIT, 2005.]]"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/367177.367199"},{"key":"e_1_3_2_1_32_1","volume-title":"June","author":"McCune W.","year":"2001","unstructured":"W. McCune . MACE 2.0 Reference Manual and Guide. ArXiv Computer Science e-prints , June 2001 .]] W. McCune. MACE 2.0 Reference Manual and Guide. ArXiv Computer Science e-prints, June 2001.]]"},{"key":"e_1_3_2_1_33_1","volume-title":"Introduction to Mathematical Logic","author":"Mendelson E.","year":"1997","unstructured":"E. Mendelson . Introduction to Mathematical Logic . Chapman & Hall , London , 4 th edition, 1997 .]] E. Mendelson. Introduction to Mathematical Logic. Chapman & Hall, London, 4th edition, 1997.]]","edition":"4"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML (Revised)","author":"Milner R.","year":"1997","unstructured":"R. Milner , M. Tofte , R. Harper , and D. MacQueen . The Definition of Standard ML (Revised) . The MIT Press , Cambridge, Mass ., 1997 .]] R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). The MIT Press, Cambridge, Mass., 1997.]]"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378851"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/322203.322204"},{"key":"e_1_3_2_1_37_1","first-page":"1","article-title":"Decidability of second-order theories and automata on infinite trees","volume":"141","author":"Rabin M.","year":"1969","unstructured":"M. Rabin . Decidability of second-order theories and automata on infinite trees . Trans. Amer. Math. Soc. , 141 : 1 -- 35 , 1969 .]] M. Rabin. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc., 141:1--35, 1969.]]","journal-title":"Trans. Amer. Math. Soc."},{"key":"e_1_3_2_1_38_1","volume-title":"The Unified Modelling Language Reference Manual","author":"Rumbaugh J.","year":"1999","unstructured":"J. Rumbaugh , I. Jacobson , and G. Booch . The Unified Modelling Language Reference Manual . Addison-Wesley, Reading , Mass ., 1999 .]] J. Rumbaugh, I. Jacobson, and G. Booch. The Unified Modelling Language Reference Manual. Addison-Wesley, Reading, Mass., 1999.]]"},{"key":"e_1_3_2_1_39_1","volume-title":"Object-Oriented Modeling and Design","author":"Rumbaugh J. R.","year":"1991","unstructured":"J. R. Rumbaugh , M. R. Blaha , W. Lorensen , F. Eddy , and W. Premerlani . Object-Oriented Modeling and Design . Prentice Hall , Englewood Cliffs , New Jersey 07632, USA, 1991 .]] J. R. Rumbaugh, M. R. Blaha, W. Lorensen, F. Eddy, and W. Premerlani. Object-Oriented Modeling and Design. Prentice Hall, Englewood Cliffs, New Jersey 07632, USA, 1991.]]"},{"key":"e_1_3_2_1_40_1","volume-title":"Computer Algebra in Scientific Computing (CASC)","author":"Sturm T.","year":"2002","unstructured":"T. Sturm and V. Weispfenning . Quantifier elimination in term algebras: The case of finite languages . In V. G. Ganzha, E. W. Mayr, and E. V. Vorozhtsov, editors, Computer Algebra in Scientific Computing (CASC) , TUM Muenchen , 2002 .]] T. Sturm and V. Weispfenning. Quantifier elimination in term algebras: The case of finite languages. In V. G. Ganzha, E. W. Mayr, and E. V. Vorozhtsov, editors, Computer Algebra in Scientific Computing (CASC), TUM Muenchen, 2002.]]"},{"key":"e_1_3_2_1_41_1","first-page":"185","volume-title":"P. Blackburn and M. de~Rijke","author":"Treinen R.","year":"1997","unstructured":"R. Treinen . Feature trees over arbitrary structures . In P. Blackburn and M. de~Rijke , editors, Specifying Syntactic Structures, chapter 7, pages 185 -- 211 . CSLI Publications and FoLLI , 1997 .]] R. Treinen. Feature trees over arbitrary structures. In P. Blackburn and M. de~Rijke, editors, Specifying Syntactic Structures, chapter 7, pages 185--211. CSLI Publications and FoLLI, 1997.]]"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/23005.24037"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25984-8_9"},{"key":"e_1_3_2_1_44_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/978-3-540-30142-4_23","volume-title":"Theorem Proving in Higher-Order Logics","author":"Zhang T.","year":"2004","unstructured":"T. Zhang , H. B. Sipma , and Z. Manna . Term algebras with length function and bounded quantifier alternation . In Theorem Proving in Higher-Order Logics , volume 3223 of LNCS , pages 321 -- 336 , 2004 .]] T. Zhang, H. B. Sipma, and Z. Manna. Term algebras with length function and bounded quantifier alternation. In Theorem Proving in Higher-Order Logics, volume 3223 of LNCS, pages 321--336, 2004.]]"}],"event":{"name":"ESEC\/FSE05: Joint 10th European Software Engineering Conference 2005","location":"Lisbon Portugal","acronym":"ESEC\/FSE05","sponsor":["ACM Association for Computing Machinery","SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1081706.1081740","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1081706.1081740","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:08:34Z","timestamp":1750248514000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1081706.1081740"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,9]]},"references-count":42,"alternative-id":["10.1145\/1081706.1081740","10.1145\/1081706"],"URL":"https:\/\/doi.org\/10.1145\/1081706.1081740","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1095430.1081740","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2005,9]]},"assertion":[{"value":"2005-09-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}