{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:36:39Z","timestamp":1771025799948,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,10,23]],"date-time":"2019-10-23T00:00:00Z","timestamp":1571788800000},"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":[[2019,10,23]]},"DOI":"10.1145\/3359591.3359726","type":"proceedings-article","created":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T18:52:21Z","timestamp":1570733541000},"page":"46-61","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["AlleAlle: bounded relational model finding with unbounded data"],"prefix":"10.1145","author":[{"given":"Jouke","family":"Stoel","sequence":"first","affiliation":[{"name":"CWI, Netherlands"}]},{"given":"Tijs","family":"van der Storm","sequence":"additional","affiliation":[{"name":"CWI, Netherlands"}]},{"given":"Jurgen J.","family":"Vinju","sequence":"additional","affiliation":[{"name":"CWI, Netherlands"}]}],"member":"320","published-online":{"date-parts":[[2019,10,23]]},"reference":[{"key":"e_1_3_2_2_1_1","first-page":"188","volume-title":"CBSE","author":"Abate P.","unstructured":"P. Abate , R. Treinen , R. Di Cosmo , and S. Zacchiroli . MPM : a modular package manager . In CBSE , pages 179\u2014- 188 . ACM, 2011. P. Abate, R. Treinen, R. Di Cosmo, and S. Zacchiroli. MPM : a modular package manager. In CBSE, pages 179\u2014-188. ACM, 2011."},{"key":"e_1_3_2_2_2_1","first-page":"119","volume-title":"POPL","author":"Aho A.V.","unstructured":"A.V. Aho and J.D. Ullman . Universality of data retrieval languages . In POPL , pages 110\u2013 119 . ACM, 1979. A.V. Aho and J.D. Ullman. Universality of data retrieval languages. In POPL , pages 110\u2013119. ACM, 1979."},{"key":"e_1_3_2_2_3_1","first-page":"214","volume-title":"ESS","author":"Baji\u0107-Bizumi\u0107 B.","unstructured":"B. Baji\u0107-Bizumi\u0107 , C. Petitpierre , H.C. Huynh , and A. Wegmann . A model-driven environment for service design, simulation and prototyping . In ESS , pages 200\u2013 214 . Springer, 2013. B. Baji\u0107-Bizumi\u0107, C. Petitpierre, H.C. Huynh, and A. Wegmann. A model-driven environment for service design, simulation and prototyping. In ESS, pages 200\u2013214. Springer, 2013."},{"key":"e_1_3_2_2_4_1","first-page":"98","volume-title":"CAV","author":"Bansal K.","unstructured":"K. Bansal , A. Reynolds , C. Barrett , and C. Tinelli . A new decision procedure for finite sets and cardinality constraints in smt . In CAV , pages 82\u2013 98 . Springer, 2016. K. Bansal, A. Reynolds, C. Barrett, and C. Tinelli. A new decision procedure for finite sets and cardinality constraints in smt. In CAV, pages 82\u201398. Springer, 2016."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"crossref","unstructured":"C.\n      Barrett C.L.\n      Conway M.\n      Deters L.\n      Hadarean Jovanovi\u0107. \n      D. T.\n      King A.\n      Reynolds and \n      C.\n      Tinelli\n  . \n  CVC4\n  . In Ganesh Gopalakrishnan and Shaz Qadeer editors CAV volume \n  6806\n   of \n  Lecture Notes in Computer Science pages 171\u2013\n  177\n  . Springer July 2011.  C. Barrett C.L. Conway M. Deters L. Hadarean Jovanovi\u0107. D. T. King A. Reynolds and C. Tinelli. CVC4. In Ganesh Gopalakrishnan and Shaz Qadeer editors CAV volume 6806 of Lecture Notes in Computer Science pages 171\u2013177. Springer July 2011.","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_3_2_2_6_1","first-page":"14","article-title":"The smt-lib standard","volume":"13","author":"Barrett C.","year":"2010","unstructured":"C. Barrett , A. Stump , C. Tinelli , The smt-lib standard : Version 2.0. In SMT , volume 13 , page 14 , 2010 . C. Barrett, A. Stump, C. Tinelli, et al. The smt-lib standard: Version 2.0. In SMT, volume 13, page 14, 2010.","journal-title":"Version 2.0. In SMT"},{"key":"e_1_3_2_2_7_1","first-page":"199","volume-title":"TACAS","volume":"15","author":"Bj\u00f8rner N.","year":"2015","unstructured":"N. Bj\u00f8rner , A. Phan , and L. Fleckenstein . \u03bd Z - An Optimizing SMT Solver . In TACAS , volume 15 , pages 194\u2013 199 , 2015 . N. Bj\u00f8rner, A. Phan, and L. Fleckenstein. \u03bd Z - An Optimizing SMT Solver. In TACAS, volume 15, pages 194\u2013199, 2015."},{"key":"e_1_3_2_2_8_1","first-page":"48","volume-title":"A viewpointbased approach for formal safety &amp","author":"Brunel J.","year":"2014","unstructured":"J. Brunel , D. Chemouil , L. Rioux , M. Bakkali , and F. Vall\u00e9e . A viewpointbased approach for formal safety &amp ; security assessment of system architectures. In MoDeVVa , volume 1235 , pages 39\u2013 48 , 2014 . J. Brunel, D. Chemouil, L. Rioux, M. Bakkali, and F. Vall\u00e9e. A viewpointbased approach for formal safety & security assessment of system architectures. In MoDeVVa, volume 1235, pages 39\u201348, 2014."},{"key":"e_1_3_2_2_9_1","first-page":"27","volume-title":"CADE-19 Workshop: Model ComputationPrinciples","author":"Claessen K.","unstructured":"K. Claessen and N. S\u00f6rensson . New techniques that improve macestyle finite model finding . In CADE-19 Workshop: Model ComputationPrinciples , Algorithms, Applications , pages 11\u2013 27 . Citeseer, 2003. K. Claessen and N. S\u00f6rensson. New techniques that improve macestyle finite model finding. In CADE-19 Workshop: Model ComputationPrinciples, Algorithms, Applications , pages 11\u201327. Citeseer, 2003."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/362384.362685"},{"key":"e_1_3_2_2_11_1","volume-title":"EDOS deliverable WP2-D2 . 1 : Report on Formal Management of Software Dependencies. Technical report","author":"Cosmo R. Di","year":"2005","unstructured":"R. Di Cosmo . EDOS deliverable WP2-D2 . 1 : Report on Formal Management of Software Dependencies. Technical report , 2005 . URL : https:\/\/hal.inria.fr\/hal-00697463\/document . R. Di Cosmo. EDOS deliverable WP2-D2 . 1 : Report on Formal Management of Software Dependencies. Technical report, 2005. URL: https:\/\/hal.inria.fr\/hal-00697463\/document ."},{"key":"e_1_3_2_2_12_1","volume-title":"AddisonWesley","author":"Date C.J.","year":"1994","unstructured":"C.J. Date . An Introduction to Database Systems . Reading, MA , AddisonWesley , 6 th edition, 1994 . C.J. Date. An Introduction to Database Systems. Reading, MA, AddisonWesley, 6th edition, 1994.","edition":"6"},{"key":"e_1_3_2_2_13_1","first-page":"148","volume-title":"FM","author":"El Ghazi A.A.","unstructured":"A.A. El Ghazi and M. Taghdiri . Relational reasoning via smt solving . In FM , pages 133\u2013 148 . Springer, 2011. A.A. El Ghazi and M. Taghdiri. Relational reasoning via smt solving. In FM, pages 133\u2013148. Springer, 2011."},{"key":"e_1_3_2_2_14_1","first-page":"115","volume-title":"HVC","author":"Grunwald D.","unstructured":"D. Grunwald , C. Gladisch , T. Liu , M. Taghdiri , and S. Tyszberowicz . Generating jml specifications from alloy expressions . In HVC , pages 99\u2013 115 . Springer, 2014. D. Grunwald, C. Gladisch, T. Liu, M. Taghdiri, and S. Tyszberowicz. Generating jml specifications from alloy expressions. In HVC, pages 99\u2013115. Springer, 2014."},{"key":"e_1_3_2_2_15_1","volume-title":"Software Abstractions - Logic, Language, and Analysis","author":"Jackson D.","year":"2012","unstructured":"D. Jackson . Software Abstractions - Logic, Language, and Analysis . MIT press , revised edition, 2012 . D. Jackson. Software Abstractions - Logic, Language, and Analysis. MIT press, revised edition, 2012."},{"key":"e_1_3_2_2_16_1","first-page":"611","volume-title":"ASE","author":"Khalek S.A.","unstructured":"S.A. Khalek , G. Yang , L. Zhang , D. Marinov , and S. Khurshid . Testera: A tool for testing java programs using Alloy specifications . In ASE , pages 608\u2013 611 . IEEE Computer Society, 2011. S.A. Khalek, G. Yang, L. Zhang, D. Marinov, and S. Khurshid. Testera: A tool for testing java programs using Alloy specifications. In ASE, pages 608\u2013611. IEEE Computer Society, 2011."},{"key":"e_1_3_2_2_17_1","first-page":"177","volume-title":"SCAM","author":"Klint P.","unstructured":"P. Klint , T. van der Storm , and J. Vinju . RASCAL: A Domain Specific Language for Source Code Analysis and Manipulation . In SCAM , pages 168\u2013 177 . IEEE, 2009. P. Klint, T. van der Storm, and J. Vinju. RASCAL: A Domain Specific Language for Source Code Analysis and Manipulation. In SCAM, pages 168\u2013177. IEEE, 2009."},{"key":"e_1_3_2_2_18_1","volume-title":"Technical report","author":"McCune W.","year":"1994","unstructured":"W. McCune . A davis-putnam program and its application to finite first-order model search: Quasigroup existence problems. Technical report , Technical report , Argonne National Laboratory , 1994 . W. McCune. A davis-putnam program and its application to finite first-order model search: Quasigroup existence problems. Technical report, Technical report, Argonne National Laboratory, 1994."},{"key":"e_1_3_2_2_19_1","first-page":"165","volume-title":"CAV","author":"Meng B.","unstructured":"B. Meng , A. Reynolds , C. Tinelli , and Clark Barrett . Relational constraint solving in smt . In CAV , pages 148\u2013 165 . Springer, 2017. B. Meng, A. Reynolds, C. Tinelli, and Clark Barrett. Relational constraint solving in smt. In CAV, pages 148\u2013165. Springer, 2017."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.05.009"},{"key":"e_1_3_2_2_21_1","first-page":"619","volume-title":"ICSE","author":"Milicevic A.","unstructured":"A. Milicevic , J.P. Near , E. Kang , and D. Jackson . Alloy*: a generalpurpose higher-order relational constraint solver . In ICSE , pages 609\u2013 619 . IEEE Press, 2015. A. Milicevic, J.P. Near, E. Kang, and D. Jackson. Alloy*: a generalpurpose higher-order relational constraint solver. In ICSE, pages 609\u2013 619. IEEE Press, 2015."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_2_23_1","volume-title":"Choco Documentation","author":"Prud\u2019homme C.","year":"2017","unstructured":"C. Prud\u2019homme , J.G. Fages , and X. Lorca . Choco Documentation , 2017 . URL : http:\/\/www.choco-solver.org . C. Prud\u2019homme, J.G. Fages, and X. Lorca. Choco Documentation, 2017. URL: http:\/\/www.choco-solver.org ."},{"key":"e_1_3_2_2_24_1","first-page":"655","volume-title":"CAV","author":"Reynolds A.","unstructured":"A. Reynolds , C. Tinelli , A. Goel , and S. Krsti\u0107 . Finite model finding in smt . In CAV , pages 640\u2013 655 . Springer, 2013. A. Reynolds, C. Tinelli, A. Goel, and S. Krsti\u0107. Finite model finding in smt. In CAV, pages 640\u2013655. Springer, 2013."},{"key":"e_1_3_2_2_26_1","first-page":"454","volume-title":"CAV","author":"Sebastiani R.","unstructured":"R. Sebastiani and P. Trentin . Optimathsat: a tool for optimization modulo theories . In CAV , pages 447\u2013 454 . Springer, 2015. R. Sebastiani and P. Trentin. Optimathsat: a tool for optimization modulo theories. In CAV, pages 447\u2013454. Springer, 2015."},{"key":"e_1_3_2_2_27_1","first-page":"801","volume-title":"CAV","author":"Slaney J.","unstructured":"J. Slaney . Finder : Finite domain enumerator system description . In CAV , pages 798\u2013 801 . Springer, 1994. J. Slaney. Finder: Finite domain enumerator system description. In CAV , pages 798\u2013801. Springer, 1994."},{"key":"e_1_3_2_2_29_1","first-page":"341","volume-title":"FM","author":"Torlak E.","unstructured":"E. Torlak , F. Chang , and D. Jackson . Finding minimal unsatisfiable cores of declarative specifications . In FM , pages 326\u2013 341 . Springer, 2008. E. Torlak, F. Chang, and D. Jackson. Finding minimal unsatisfiable cores of declarative specifications. In FM, pages 326\u2013341. Springer, 2008."},{"key":"e_1_3_2_2_30_1","volume-title":"Alloy Workshop","author":"Torlak E.","year":"2006","unstructured":"E. Torlak and G. Dennis . Kodkod for Alloy users . In Alloy Workshop , 2006 . E. Torlak and G. Dennis. Kodkod for Alloy users. In Alloy Workshop, 2006."},{"key":"e_1_3_2_2_31_1","first-page":"647","volume-title":"TACAS","author":"Torlak E.","unstructured":"E. Torlak and D. Jackson . Kodkod: A relational model finder . In TACAS , pages 632\u2013 647 . Springer, 2007. E. Torlak and D. Jackson. Kodkod: A relational model finder. In TACAS, pages 632\u2013647. Springer, 2007."},{"key":"e_1_3_2_2_32_1","first-page":"188","volume-title":"ICSE","author":"Tucker C.","unstructured":"C. Tucker , D. Shuffelton , R. Jhala , and S. Lerner . Opium: Optimal package install\/uninstall manager . In ICSE , pages 178\u2013 188 . IEEE Computer Society, 2007. C. Tucker, D. Shuffelton, R. Jhala, and S. Lerner. Opium: Optimal package install\/uninstall manager. In ICSE, pages 178\u2013188. IEEE Computer Society, 2007."},{"key":"e_1_3_2_2_33_1","first-page":"693","volume-title":"FM","author":"Vakili A.","unstructured":"A. Vakili and N.A. Day . Finite model finding using the logic of equality with uninterpreted functions . In FM , pages 677\u2013 693 . Springer, 2016. A. Vakili and N.A. Day. Finite model finding using the logic of equality with uninterpreted functions. In FM, pages 677\u2013693. Springer, 2016."},{"key":"e_1_3_2_2_34_1","first-page":"303","volume-title":"IJCAI","volume":"95","author":"Zhang J.","year":"1995","unstructured":"J. Zhang and H. Zhang . Sem: a system for enumerating models . In IJCAI , volume 95 , pages 298\u2013 303 , 1995 . J. Zhang and H. Zhang. Sem: a system for enumerating models. In IJCAI , volume 95, pages 298\u2013303, 1995."}],"event":{"name":"SPLASH '19: 2019 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity","location":"Athens Greece","acronym":"SPLASH '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 2019 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3359591.3359726","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3359591.3359726","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:23:06Z","timestamp":1750202586000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3359591.3359726"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,23]]},"references-count":32,"alternative-id":["10.1145\/3359591.3359726","10.1145\/3359591"],"URL":"https:\/\/doi.org\/10.1145\/3359591.3359726","relation":{},"subject":[],"published":{"date-parts":[[2019,10,23]]},"assertion":[{"value":"2019-10-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}