{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:37:52Z","timestamp":1781239072501,"version":"3.54.1"},"reference-count":68,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T00:00:00Z","timestamp":1714348800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"U.S. National Science Foundation","award":["SHF-2227863,SaTC-2208731,CCF-2030859"],"award-info":[{"award-number":["SHF-2227863,SaTC-2208731,CCF-2030859"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,4,29]]},"abstract":"<jats:p>\n            This paper presents the design of\n            <jats:italic>Forge<\/jats:italic>\n            , a tool for teaching formal methods gradually. Forge is based on the widely-used Alloy language and analysis tool, but contains numerous improvements based on more than a decade of experience teaching Alloy to students. Although our focus has been on the classroom, many of the ideas in Forge likely also apply to training in industry.\n          <\/jats:p>\n          <jats:p>\n            Forge offers a\n            <jats:italic>progression of languages<\/jats:italic>\n            that improve the learning experience by only gradually increasing in expressive power. Forge supports\n            <jats:italic>custom visualization<\/jats:italic>\n            of its outputs, enabling the use of widely-understood domain-specific representations. Finally, Forge provides a variety of\n            <jats:italic>testing features<\/jats:italic>\n            to ease the transition from programming to formal modeling. We present the motivation for and design of these aspects of Forge, and then provide a substantial evaluation based on multiple years of classroom use.\n          <\/jats:p>","DOI":"10.1145\/3649833","type":"journal-article","created":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:53:50Z","timestamp":1714413230000},"page":"613-641","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Forge: A Tool and Language for Teaching Formal Methods"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9377-9943","authenticated-orcid":false,"given":"Tim","family":"Nelson","sequence":"first","affiliation":[{"name":"Brown University, Providence, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7078-9287","authenticated-orcid":false,"given":"Ben","family":"Greenman","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7936-8147","authenticated-orcid":false,"given":"Siddhartha","family":"Prasad","sequence":"additional","affiliation":[{"name":"Brown University, Providence, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9730-9319","authenticated-orcid":false,"given":"Tristan","family":"Dyer","sequence":"additional","affiliation":[{"name":"Stashpad, Raleigh, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-9484-8745","authenticated-orcid":false,"given":"Ethan","family":"Bove","sequence":"additional","affiliation":[{"name":"Brown University, Providence, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-6742-4089","authenticated-orcid":false,"given":"Qianfan","family":"Chen","sequence":"additional","affiliation":[{"name":"Brown University, Providence, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-2528-7645","authenticated-orcid":false,"given":"Charles","family":"Cutting","sequence":"additional","affiliation":[{"name":"Brown University, Providence, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-1472-0045","authenticated-orcid":false,"given":"Thomas","family":"Del Vecchio","sequence":"additional","affiliation":[{"name":"Brown University, Providence, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-9931-5594","authenticated-orcid":false,"given":"Sidney","family":"LeVine","sequence":"additional","affiliation":[{"name":"Brown University, Providence, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-5452-7098","authenticated-orcid":false,"given":"Julianne","family":"Rudner","sequence":"additional","affiliation":[{"name":"Brown University, Providence, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-1329-3858","authenticated-orcid":false,"given":"Ben","family":"Ryjikov","sequence":"additional","affiliation":[{"name":"Brown University, Providence, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-8611-6444","authenticated-orcid":false,"given":"Alexander","family":"Varga","sequence":"additional","affiliation":[{"name":"Brown University, Providence, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9434-0780","authenticated-orcid":false,"given":"Andrew","family":"Wagner","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-9005-7513","authenticated-orcid":false,"given":"Luke","family":"West","sequence":"additional","affiliation":[{"name":"Brown University, Providence, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5184-1975","authenticated-orcid":false,"given":"Shriram","family":"Krishnamurthi","sequence":"additional","affiliation":[{"name":"Brown University, Providence, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,4,29]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Alloy Analyzer Downloads. https:\/\/alloytools.org\/download.html Accessed","year":"2023","unstructured":"alloytools.org. 2023. Alloy Analyzer Downloads. https:\/\/alloytools.org\/download.html Accessed August 27, 2023"},{"key":"e_1_2_1_2_1","unstructured":"alloytools.org. 2023. Case study applications of Alloy. http:\/\/alloytools.org\/citations\/case-studies.html Accessed August 1 2023"},{"key":"e_1_2_1_3_1","unstructured":"alloytools.org. 2023. Courses using Alloy. http:\/\/alloytools.org\/citations\/courses.html Accessed August 1 2023"},{"key":"e_1_2_1_4_1","unstructured":"alloytools.org. 2023. Translation into Alloy. http:\/\/alloytools.org\/citations\/language-translations.html Accessed August 1 2023"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428290"},{"key":"e_1_2_1_6_1","unstructured":"Christoph Beierle Marjaa Kulaa and Manfred Widera. 2003. Automatic Analysis of Programming Assignments. In DeLFI. GI 144\u2013153. https:\/\/dl.gi.de\/handle\/20.500.12116\/15081"},{"key":"e_1_2_1_7_1","unstructured":"Christoph Beierle Marija Kula\u0161 and Manfred Widera. 2004. Partial Specifications of Program Properties. In TeachLP. 17 pages. https:\/\/ep.liu.se\/ecp\/012\/ecp04012.pdf"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11415763_20"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.139.6"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1561\/3300000004"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-33163-3_16"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2006.08.041"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","unstructured":"Ravi Chugh Brian Hempel Mitchell Spradlin and Jacob Albers. 2016. Programmatic and Direct Manipulation Together at Last. In PLDI. ACM 341\u2013354. https:\/\/doi.org\/10.1145\/2908080.2908103 10.1145\/2908080.2908103","DOI":"10.1145\/2908080.2908103"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","unstructured":"Koen Claessen and John Hughes. 2000. QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs. In ICFP. ACM 268\u2013279. https:\/\/doi.org\/10.1145\/357766.351266 10.1145\/357766.351266","DOI":"10.1145\/357766.351266"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.284.4"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","unstructured":"Leonardo de Moura and N. Bj\u00f8rner. 2008. Z3: An efficient SMT solver. In TACAS. Springer 337\u2013340. https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24 10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146251"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3364510.3366170"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_41"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1006\/IJHC.1981.0309"},{"key":"e_1_2_1_24_1","volume-title":"Lightweight Formal Methods in Scientific Computing. Ph. D. Dissertation","author":"Dyer Andrew Tristan","unstructured":"Andrew Tristan Dyer. 2020. Lightweight Formal Methods in Scientific Computing. Ph. D. Dissertation. North Carolina State University. https:\/\/repository.lib.ncsu.edu\/items\/95554653-06ab-4a76-adbd-846f2c9b995f"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-77543-8_7"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","unstructured":"Jonathan Edwards Daniel Jackson and Emina Torlak. 2004. A Type System for Object Models. In FSE. ACM 189\u2013199. https:\/\/doi.org\/10.1145\/1029894.1029921 10.1145\/1029894.1029921","DOI":"10.1145\/1029894.1029921"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE59848.2023.00065"},{"key":"e_1_2_1_28_1","volume-title":"Matthew Flatt, and Shriram Krishnamurthi.","author":"Felleisen Matthias","year":"2001","unstructured":"Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, and Shriram Krishnamurthi. 2001. How to Design Programs. MIT Press. isbn:978-0-262-53480-2 http:\/\/www.htdp.org\/"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127323"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.113"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004208"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.COLA.2022.101158"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.22152\/programming-journal.org"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180165"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/800183.810456"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/2029108"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_6"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/2141100"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338843"},{"key":"e_1_2_1_41_1","volume-title":"Lightweight Formal Methods","author":"Jackson Daniel","unstructured":"Daniel Jackson and Jeanette Wing. 1996. Lightweight Formal Methods. IEEE Computer, https:\/\/people.csail.mit.edu\/dnj\/publications\/ieee96-roundtable.html"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jvlc.2017.04.005"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-022-09642-2"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","unstructured":"Nuno Macedo Julien Brunel David Chemouil Alcino Cunha and Denis Kuperberg. 2016. Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations. In FSE. ACM 373\u2013383. https:\/\/doi.org\/10.1145\/2950290.2950318 10.1145\/2950290.2950318","DOI":"10.1145\/2950290.2950318"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2021.102690"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88313-5_34"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30885-7_9"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.10463960"},{"key":"e_1_2_1_50_1","unstructured":"Ulrich Neumerkel and Stefan Kral. 2002. Declarative Program Development in Prolog with GUPU. In WLPE. 77\u201386. arxiv:cs\/0207044"},{"key":"e_1_2_1_51_1","unstructured":"Ulrich Neumerkel Christoph Rettig and Christian Schallart. 1997. Visualizing Solutions with Viewers. In LPE. 43\u201350. https:\/\/www.complang.tuwien.ac.at\/ulrich\/papers\/PDF\/wlpe97.pdf"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_1_53_1","volume-title":"D3: Data-Driven Documents. https:\/\/d3js.org Accessed","year":"2023","unstructured":"Observable. 2023. D3: Data-Driven Documents. https:\/\/d3js.org Accessed August 25, 2023"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.14279\/tuj.eceasst.7.94"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3122826"},{"key":"e_1_2_1_56_1","volume-title":"Query Strategies for Directed Graphical Models and their Application to Adaptive Testing. Ph. D. Dissertation","author":"Saarinen Sam","unstructured":"Sam Saarinen. 2021. Query Strategies for Directed Graphical Models and their Application to Adaptive Testing. Ph. D. Dissertation. Brown University. https:\/\/repository.library.brown.edu\/studio\/item\/bdr:kgyft3b4\/"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-91631-2_22"},{"key":"e_1_2_1_58_1","volume-title":"Z Notation \u2014 A Reference Manual","author":"Spivey J. Michael","unstructured":"J. Michael Spivey. 1992. Z Notation \u2014 A Reference Manual (2nd ed.). Prentice Hall. isbn:978-0-13-978529-0","edition":"2"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2018.00047"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","unstructured":"Emina Torlak and Rastislav Bodik. 2014. A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages. In PLDI. ACM 530\u2013541. https:\/\/doi.org\/10.1145\/2594291.2594340 10.1145\/2594291.2594340","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","unstructured":"Preston Tunnell Wilson Ben Greenman Justin Pombrio and Shriram Krishnamurthi. 2018. The Behavior of Gradual Types: a User Study. In DLS. ACM 1\u201312. https:\/\/doi.org\/10.1145\/3276945.3276947 10.1145\/3276945.3276947","DOI":"10.1145\/3276945.3276947"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","unstructured":"Kaiyuan Wang Allison Sullivan and Sarfraz Khurshid. 2018. Automated Model Repair for Alloy. In ASE. ACM 577\u2013588. https:\/\/doi.org\/10.1145\/3238147.3238162 10.1145\/3238147.3238162","DOI":"10.1145\/3238147.3238162"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE5003.2020.00044"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","unstructured":"Aaron Wilson Margaret Burnett Laura Beckwith Orion Granatir Ledah Casburn Curtis Cook Mike Durham and Gregg Rothermel. 2003. Harnessing Curiosity to Increase Correctness in End-User Programming. In CHI. ACM 305\u2013312. https:\/\/doi.org\/10.1145\/642611.642665 10.1145\/642611.642665","DOI":"10.1145\/642611.642665"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","unstructured":"John Wrenn Shriram Krishnamurthi and Kathi Fisler. 2018. Who Tests the Testers? In ICER. ACM 51\u201359. https:\/\/doi.org\/10.1145\/3230977.3230999 10.1145\/3230977.3230999","DOI":"10.1145\/3230977.3230999"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.22152\/programming-journal.org"},{"key":"e_1_2_1_67_1","volume-title":"Executable Examples: Empowering Students to Hone Their Problem Comprehension. Ph. D. Dissertation","author":"Wrenn John Sinclair","year":"2022","unstructured":"John Sinclair Wrenn. 2022. Executable Examples: Empowering Students to Hone Their Problem Comprehension. Ph. D. Dissertation. Brown University. https:\/\/cs.brown.edu\/research\/pubs\/theses\/phd\/2022\/wrenn.john.pdf"},{"key":"e_1_2_1_68_1","volume-title":"Discourse Forum Reply. https:\/\/alloytools.discourse.group\/t\/visualization-for-alloy-what-do-you-want\/111\/2 Accessed","author":"Zave Pamela","year":"2023","unstructured":"Pamela Zave. 2020. Discourse Forum Reply. https:\/\/alloytools.discourse.group\/t\/visualization-for-alloy-what-do-you-want\/111\/2 Accessed August 22, 2023"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649833","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649833","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:06Z","timestamp":1750287246000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649833"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,29]]},"references-count":68,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2024,4,29]]}},"alternative-id":["10.1145\/3649833"],"URL":"https:\/\/doi.org\/10.1145\/3649833","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,29]]},"assertion":[{"value":"2024-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}