{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:36:43Z","timestamp":1771025803023,"version":"3.50.1"},"reference-count":41,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"2","license":[{"start":{"date-parts":[[2023,2,1]],"date-time":"2023-02-01T00:00:00Z","timestamp":1675209600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2023,2,1]],"date-time":"2023-02-01T00:00:00Z","timestamp":1675209600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,2,1]],"date-time":"2023-02-01T00:00:00Z","timestamp":1675209600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2023,2,1]]},"DOI":"10.1109\/tse.2022.3162985","type":"journal-article","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T19:47:03Z","timestamp":1648583223000},"page":"743-759","source":"Crossref","is-referenced-by-count":6,"title":["Static Profiling of Alloy Models"],"prefix":"10.1109","volume":"49","author":[{"given":"Elias","family":"Eid","sequence":"first","affiliation":[{"name":"David R. Cheriton School of Computer Science, University of Waterloo, Waterloo, ON, 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, Waterloo, ON, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"key":"ref2","volume-title":"Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport","year":"2002"},{"key":"ref3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book - Assigning Programs to Meanings","author":"Abrial","year":"1996"},{"key":"ref4","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B - System and Software Engineering","author":"Abrial","year":"2010"},{"key":"ref5","volume-title":"Z Notation - A Reference Manual","author":"Spivey","year":"1992"},{"key":"ref6","volume-title":"Systematic Software Development Using VDM","author":"Jones","year":"1991"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-736-3_3"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2185376.2185383"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxz039"},{"key":"ref11","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson","year":"2012"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4842-3829-5"},{"key":"ref13","volume-title":"ABZ 2021\u20138th International Conference on Rigorous State Based Methods","year":"2021"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07512-9_1"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-48077-6_15"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.206.5"},{"key":"ref17","article-title":"Evaluating state modeling techniques in Alloy","volume-title":"Proc. 6th Workshop Softw. Qual. Anal. Monit. Improvement Appl.","author":"Sullivan"},{"key":"ref18","article-title":"Logic for systems","author":"Nelson","year":"2022"},{"key":"ref19","article-title":"M\u00e9todos Formais de Programa\u00e7\u00e3o","author":"Cunha","year":"2021"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17404-4_7"},{"key":"ref21","first-page":"81","article-title":"Introducing Alloy in a software modelling course","volume-title":"Proc. Formal Methods Comput. Sci. Educ. Workshop","author":"Noble"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/2663342"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1016\/s0065-2458(02)80005-5"},{"key":"ref24","article-title":"SDMetrics","author":"W\u00fcst","year":"2021"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1016\/j.sysarc.2010.06.003"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-019-00763-8"},{"key":"ref29","article-title":"A comprehensive study of declarative modelling languages","author":"Bandali","year":"2020"},{"key":"ref30","article-title":"Linking alloy with SMT-based finite model finding","author":"Tariq","year":"2021"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/3338843"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_49"},{"key":"ref34","article-title":"Catalyst","author":"Yan","year":"2021"},{"key":"ref35","article-title":"Static profiling of Alloy models","author":"Eid","year":"2022"},{"key":"ref36","volume-title":"The Definitive ANTLR 4 Reference","author":"Parr","year":"2013"},{"key":"ref41","article-title":"Profiling Alloy models","author":"Eid","year":"2021"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/REW53955.2021.00010"},{"key":"ref43","first-page":"143","article-title":"Coupling and cohesion (towards a valid metrics suite for object-oriented analysis and design)","volume":"3","author":"Henderson-Sellers","year":"1996","journal-title":"Object Oriented Syst."},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2019.00031"},{"key":"ref46","article-title":"Alloy\/kodkod benchmarks","author":"Erata","year":"2018"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45234-6_2"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/2858965.2814300"},{"key":"ref49","first-page":"78","article-title":"Lint, A C Program Checker","author":"Johnson","year":"1978","journal-title":"Comp. Sci. Tech. Rep"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/10044379\/09744446.pdf?arnumber=9744446","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,18]],"date-time":"2024-01-18T00:43:29Z","timestamp":1705538609000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9744446\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,2,1]]},"references-count":41,"journal-issue":{"issue":"2"},"URL":"https:\/\/doi.org\/10.1109\/tse.2022.3162985","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,2,1]]}}}