{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:36:32Z","timestamp":1771025792130,"version":"3.50.1"},"reference-count":37,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2023]]},"DOI":"10.1109\/tse.2023.3256939","type":"journal-article","created":{"date-parts":[[2023,3,14]],"date-time":"2023-03-14T17:27:55Z","timestamp":1678814875000},"page":"1-17","source":"Crossref","is-referenced-by-count":1,"title":["New Techniques for Static Symmetry Breaking in Many-Sorted Finite Model Finding"],"prefix":"10.1109","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3210-5504","authenticated-orcid":false,"given":"Joseph","family":"Poremba","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of British Columbia, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1422-692X","authenticated-orcid":false,"given":"Nancy A.","family":"Day","sequence":"additional","affiliation":[{"name":"David R. Cheriton School of Computer Science, University of Waterloo, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amirhossein","family":"Vakili","sequence":"additional","affiliation":[{"name":"David R. Cheriton School of Computer Science, University of Waterloo, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref1","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson","year":"2012"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jisa.2019.01.008"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/2185376.2185383"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/1656485.1656489"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.procs.2014.08.072"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_27"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/Correctness49594.2019.00010"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-48077-6_4"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30885-7_11"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3240475"},{"key":"ref11","first-page":"171","article-title":"CVC4","volume-title":"Proc. Int. Conf. Comput.-Aided Verification","author":"Barrett"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_42"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_26"},{"key":"ref14","article-title":"A Davis-Putnam program and its application to finite first-order model search: QuasiGroup existence problem","author":"McCune","year":"1994"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36675-8_5"},{"key":"ref16","first-page":"11","article-title":"New techniques that improve MACE-style finite model finding","volume-title":"Proc. Conf. Automated Deduction","author":"Claessen"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_49"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_41"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.2172\/822574"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/775832.776042"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45190-5_7"},{"key":"ref22","article-title":"A constraint solver for software engineering: Finding models and cores of large relational specifications","author":"Torlak","year":"2009"},{"key":"ref23","article-title":"The SMT-LIB standard: Version 2.6","author":"Barrett","year":"2017"},{"key":"ref24","first-page":"298","article-title":"SEM: A system for enumerating models","volume-title":"Proc. Int. Joint Conf. Artif. Intell. Org.","author":"Zhang"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_20"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/BF00247667"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/8.4.511"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2007.07.005"},{"key":"ref29","first-page":"1","article-title":"Symmetry in finite model of first order logic","volume-title":"Proc. Workshop Symmetry Constraint Satisfaction Problems\u2013Affiliated CP","author":"Audemard"},{"key":"ref30","first-page":"148","article-title":"Symmetry-breaking predicates for search problems","volume-title":"Proc. 5th Int. Conf. Princ. Knowl. Representation Reasoning","author":"Crawford"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29007-8_1"},{"key":"ref32","volume-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1016\/S1574-6526(06)80014-3"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-006-8059-8"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61511-3_96"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2005.10.018"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/4359463\/10068805.pdf?arnumber=10068805","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,3]],"date-time":"2024-03-03T05:11:01Z","timestamp":1709442661000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10068805\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"references-count":37,"URL":"https:\/\/doi.org\/10.1109\/tse.2023.3256939","relation":{},"ISSN":["0098-5589","1939-3520","2326-3881"],"issn-type":[{"value":"0098-5589","type":"print"},{"value":"1939-3520","type":"electronic"},{"value":"2326-3881","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]}}}