{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,18]],"date-time":"2026-07-18T16:38:05Z","timestamp":1784392685788,"version":"3.55.0"},"reference-count":67,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2013,7,8]],"date-time":"2013-07-08T00:00:00Z","timestamp":1373241600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2013,8]]},"abstract":"<jats:p>Alloy is a declarative language for lightweight modelling and analysis of software. The core of the language is based on first-order relational logic, which offers an attractive balance between analysability and expressiveness. The logic is expressive enough to capture the intricacies of real systems, but is also simple enough to support fully automated analysis with the Alloy Analyzer. The Analyzer is built on a SAT-based constraint solver and provides automated simulation, checking and debugging of Alloy specifications. Because of its automated analysis and expressive logic, Alloy has been applied in a wide variety of domains. These applications have motivated a number of extensions both to the Alloy language and to its SAT-based analysis. This paper provides an overview of Alloy in the context of its three largest application domains, lightweight modelling, bounded code verification and test-case generation, and three recent application-driven extensions, an imperative extension to the language, a compiler to executable code and a proof-capable analyser based on SMT.<\/jats:p>","DOI":"10.1017\/s0960129512000291","type":"journal-article","created":{"date-parts":[[2013,7,8]],"date-time":"2013-07-08T11:28:01Z","timestamp":1373282881000},"page":"915-933","source":"Crossref","is-referenced-by-count":13,"title":["Applications and extensions of Alloy: past, present and future"],"prefix":"10.1017","volume":"23","author":[{"given":"EMINA","family":"TORLAK","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"MANA","family":"TAGHDIRI","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"GREG","family":"DENNIS","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"JOSEPH P.","family":"NEAR","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2013,7,8]]},"reference":[{"key":"S0960129512000291_ref67","unstructured":"Yeung V. (2006) Declarative configuration applied to course scheduling. Master's thesis, Massachusetts Institute of Technology, Cambridge, MA."},{"key":"S0960129512000291_ref63","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2008.56"},{"key":"S0960129512000291_ref62","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.424"},{"key":"S0960129512000291_ref61","doi-asserted-by":"publisher","DOI":"10.1145\/1809028.1806635"},{"key":"S0960129512000291_ref59","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_23"},{"key":"S0960129512000291_ref58","unstructured":"Torlak E. (2009) A constraint solver for software engineering: finding models and cores of large relational specifications, Ph.D. thesis, MIT."},{"key":"S0960129512000291_ref56","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181809"},{"key":"S0960129512000291_ref55","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-006-0005-x"},{"key":"S0960129512000291_ref54","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39979-7_16"},{"key":"S0960129512000291_ref53","unstructured":"Taghdiri M. (2007) Automating Modular Program Verification by Refining Specifications, Ph.D. thesis, Massachusetts Institute of Technology."},{"key":"S0960129512000291_ref52","unstructured":"Stepney S. , Cooper D. and Woodcock J. (2000) An electronic purse: Specification, refinement and proof. Technical report, Oxford University Computing Laboratory, Programming Research Group."},{"key":"S0960129512000291_ref51","unstructured":"Spivey J. M. (1992) The Z Notation: A Reference Manual, International Series in Computer Science, Prentice Hall."},{"key":"S0960129512000291_ref50","unstructured":"Spiridonov A. and Khurshid S. (2007) Pythia: Automatic generation of counterexamples for ACL2 using Alloy. In: Proceedings of the 7th International Workshop on the ACL2 Theorem Prover and its Applications."},{"key":"S0960129512000291_ref47","doi-asserted-by":"publisher","DOI":"10.1007\/s00766-007-0048-y"},{"key":"S0960129512000291_ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11811-1_10"},{"key":"S0960129512000291_ref40","first-page":"144","article-title":"From relational specifications to logic programs","volume":"7","author":"Near","year":"2010","journal-title":"Leibniz International Proceedings in Informatics"},{"key":"S0960129512000291_ref38","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.04.003"},{"key":"S0960129512000291_ref36","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1145\/1040305.1040336","volume-title":"Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages: POPL '05","author":"Manson","year":"2005"},{"key":"S0960129512000291_ref39","doi-asserted-by":"publisher","DOI":"10.1007\/s10922-008-9108-y"},{"key":"S0960129512000291_ref37","volume-title":"Proceedings of the 16th IEEE International Conference on Automated Software Engineering: ASE '01","author":"Marinov","year":"2001"},{"key":"S0960129512000291_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_3"},{"key":"S0960129512000291_ref21","unstructured":"Galeotti J. P. (2010) Software Verification using Alloy, Ph.D. thesis, University of Buenos Aires."},{"key":"S0960129512000291_ref14","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.21.7"},{"key":"S0960129512000291_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55602-8_217"},{"key":"S0960129512000291_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_12"},{"key":"S0960129512000291_ref66","doi-asserted-by":"publisher","DOI":"10.3233\/MGS-2006-2410"},{"key":"S0960129512000291_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-009-9153-6"},{"key":"S0960129512000291_ref44","doi-asserted-by":"publisher","DOI":"10.1145\/1808266.1808276"},{"key":"S0960129512000291_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"S0960129512000291_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0058-z"},{"key":"S0960129512000291_ref65","unstructured":"Vaziri M. (2004) Finding Bugs in Software with a Constraint Solver, Ph.D. thesis, Massachusetts Institute of Technology, Cambridge, MA."},{"key":"S0960129512000291_ref6","doi-asserted-by":"crossref","unstructured":"Blanchette J. and Nipkow T. (2009) Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: TAP 2009: short papers. Technical report tr630, ETH Zurich.","DOI":"10.1007\/978-3-642-14052-5_11"},{"key":"S0960129512000291_ref10","unstructured":"Dennis G. (2009) A relational framework for bounded program verification, Ph.D. thesis, Massachusetts Institute of Technology."},{"key":"S0960129512000291_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/509252.509264"},{"key":"S0960129512000291_ref12","doi-asserted-by":"publisher","DOI":"10.1145\/1007512.1007535"},{"key":"S0960129512000291_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24771-5_3"},{"key":"S0960129512000291_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146251"},{"key":"S0960129512000291_ref46","unstructured":"Sakai M. and Imai T. (2009) CForge: A bounded verifier for the C language. In: The 11th Programming and Programming Language workshop (PPL '09)."},{"key":"S0960129512000291_ref28","unstructured":"Hynix Semiconductor et al. (2006) Open NAND flash interface specification. Technical report, ONFi Workgroup."},{"key":"S0960129512000291_ref64","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_22"},{"key":"S0960129512000291_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"S0960129512000291_ref45","volume-title":"The Theory and Practice of Concurrency","author":"Roscoe","year":"2005"},{"key":"S0960129512000291_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16901-4_38"},{"key":"S0960129512000291_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/1284680.1284683"},{"key":"S0960129512000291_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_18"},{"key":"S0960129512000291_ref60","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_49"},{"key":"S0960129512000291_ref8","unstructured":"Chang F. (2007) Alloy analyzer 4.0. (Available at http:\/\/Alloy.mit.edu\/Alloy4\/.)"},{"key":"S0960129512000291_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/1089733.1089735"},{"key":"S0960129512000291_ref34","doi-asserted-by":"publisher","DOI":"10.1145\/1453101.1453123"},{"key":"S0960129512000291_ref5","first-page":"193","article-title":"Symbolic model checking without BDDs","volume":"3","author":"Biere","year":"1999","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"S0960129512000291_ref57","unstructured":"The Open Group (2003) The POSIX 1003.1, 2003 edition specification. (Available at: http:\/\/www.opengroup.org\/certification\/idx\/posix.html.)"},{"key":"S0960129512000291_ref27","volume-title":"The Spin model checker","author":"Holzmann","year":"2004"},{"key":"S0960129512000291_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831712"},{"key":"S0960129512000291_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859063"},{"key":"S0960129512000291_ref2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"S0960129512000291_ref3","unstructured":"Arkoudas K. (2000) Denotational Proof Languages, Ph.D. thesis, Massachusetts Institute of Technology."},{"key":"S0960129512000291_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_3"},{"key":"S0960129512000291_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/320434.320440"},{"key":"S0960129512000291_ref13","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287653"},{"key":"S0960129512000291_ref17","first-page":"442","volume-title":"Proceedings of the 27th International Conference on Software Engineering \u2013 ICSE '05","author":"Frias","year":"2005"},{"key":"S0960129512000291_ref29","unstructured":"Ives B. and Earl M. (1997) Mondex international: Reengineering money. Technical Report CRIM CS97\/2, London Business School."},{"key":"S0960129512000291_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87603-8_23"},{"key":"S0960129512000291_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_46"},{"key":"S0960129512000291_ref30","volume-title":"Software Abstractions: logic, language, and analysis","author":"Jackson","year":"2006"},{"key":"S0960129512000291_ref49","doi-asserted-by":"publisher","DOI":"10.1145\/1512762.1512764"},{"key":"S0960129512000291_ref32","first-page":"129","article-title":"Designing and analyzing a flash file system with Alloy.","volume":"3","author":"Kang","year":"2009","journal-title":"International Journal of Software and Informatics"},{"key":"S0960129512000291_ref33","first-page":"238","volume-title":"Proceedings of the 23rd IEEE\/ACM International Conference on Automated Software Engineering: ASE '08","author":"Khalek","year":"2008"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129512000291","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,27]],"date-time":"2022-02-27T18:01:48Z","timestamp":1645984908000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129512000291\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7,8]]},"references-count":67,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,8]]}},"alternative-id":["S0960129512000291"],"URL":"https:\/\/doi.org\/10.1017\/s0960129512000291","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,7,8]]}}}