{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,20]],"date-time":"2026-09-20T05:17:23Z","timestamp":1789881443976,"version":"4.0.1"},"reference-count":18,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2007,12,1]],"date-time":"2007-12-01T00:00:00Z","timestamp":1196467200000},"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":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2007,12]]},"abstract":"<jats:p>\n            DynAlloy is an extension of Alloy to support the definition of actions and the specification of assertions regarding execution traces. In this article we show how we can extend the Alloy tool so that DynAlloy specifications can be automatically analyzed in an efficient way. We also demonstrate that DynAlloy's semantics allows for a sound technique that we call\n            <jats:italic>program atomization<\/jats:italic>\n            , which improves the analyzability of properties regarding execution traces by considering certain programs as atomic steps in a trace.\n          <\/jats:p>\n          <jats:p>We present the foundations, case studies, and empirical results indicating that the analysis of DynAlloy specifications can be performed efficiently.<\/jats:p>","DOI":"10.1145\/1314493.1314497","type":"journal-article","created":{"date-parts":[[2008,1,18]],"date-time":"2008-01-18T18:45:29Z","timestamp":1200681929000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Efficient Analysis of DynAlloy Specifications"],"prefix":"10.1145","volume":"17","author":[{"given":"Marcelo F.","family":"Frias","sequence":"first","affiliation":[{"name":"Universidad de Buenos Aires"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Carlos G.","family":"Lopez Pombo","sequence":"additional","affiliation":[{"name":"Universidad de Buenos Aires"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Juan P.","family":"Galeotti","sequence":"additional","affiliation":[{"name":"Universidad de Buenos Aires"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nazareno M.","family":"Aguirre","sequence":"additional","affiliation":[{"name":"Universidad Nacional de R\u00edo Cuarto"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2007,12,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Dijkstra E. W. and Scholten C. S. 1990. Predicate Calculus and Program Semantics. Springer-Verlag New York NY.   Dijkstra E. W. and Scholten C. S. 1990. Predicate Calculus and Program Semantics. Springer-Verlag New York NY.","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"e_1_2_1_3_1","first-page":"19","volume-title":"Proceedings of Symposia in Applied Mathematics. American Mathematical Society","author":"Floyd R. W.","year":"1967","unstructured":"Floyd , R. W. 1967 . Assigning meanings to programs. In Mathematical Aspects of Computer Science , Proceedings of Symposia in Applied Mathematics. American Mathematical Society , Providence, Rhode Island , pp. 19 -- 32 . Floyd, R. W. 1967. Assigning meanings to programs. In Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics. American Mathematical Society, Providence, Rhode Island, pp. 19--32."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062535"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the Sixth International Conference on Formal Engineering Methods (ICFEM), J. Davies, W. Schulte, and M. Barnett, Eds. Lecture Notes in Computer Science","volume":"3308","author":"Frias M. F.","unstructured":"Frias , M. F. , Lopez Pombo , C. G. , and Aguirre , N. M . 2004. An equational calculus for Alloy . In Proceedings of the Sixth International Conference on Formal Engineering Methods (ICFEM), J. Davies, W. Schulte, and M. Barnett, Eds. Lecture Notes in Computer Science , vol. 3308 . Springer-Verlag, Seattle, Washington, 162--175. Frias, M. F., Lopez Pombo, C. G., and Aguirre, N. M. 2004. An equational calculus for Alloy. In Proceedings of the Sixth International Conference on Formal Engineering Methods (ICFEM), J. Davies, W. Schulte, and M. Barnett, Eds. Lecture Notes in Computer Science, vol. 3308. Springer-Verlag, Seattle, Washington, 162--175."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1101815.1101819"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the Conference on Design, Automation and, Test in Europe, C. D. Kloos and J. da Franca, Eds. IEEE Computer Society","author":"Goldberg E.","unstructured":"Goldberg , E. and Novikov , Y . 2002. BerkMin: A fast and robust SAT-solver . In Proceedings of the Conference on Design, Automation and, Test in Europe, C. D. Kloos and J. da Franca, Eds. IEEE Computer Society , Paris, France, 142--149. Goldberg, E. and Novikov, Y. 2002. BerkMin: A fast and robust SAT-solver. In Proceedings of the Conference on Design, Automation and, Test in Europe, C. D. Kloos and J. da Franca, Eds. IEEE Computer Society, Paris, France, 142--149."},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Harel D. Kozen D. and Tiuryn J. 2000. Dynamic logic. Foundations of Computing. MIT Press Cambridge MA.   Harel D. Kozen D. and Tiuryn J. 2000. Dynamic logic. Foundations of Computing. MIT Press Cambridge MA.","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"key":"e_1_2_1_11_1","volume-title":"Micromodels of Software: Lightweight Modelling and Analysis with Alloy. MIT Laboratory for Computer Science","author":"Jackson D.","unstructured":"Jackson , D. 2002b. Micromodels of Software: Lightweight Modelling and Analysis with Alloy. MIT Laboratory for Computer Science , Cambridge, MA . Jackson, D. 2002b. Micromodels of Software: Lightweight Modelling and Analysis with Alloy. MIT Laboratory for Computer Science, Cambridge, MA."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503219"},{"key":"e_1_2_1_13_1","volume-title":"Systematic Software Development Using VDM","author":"Jones C.","unstructured":"Jones , C. 1986. Systematic Software Development Using VDM . Prentice Hall , Hertfordshire, UK . Jones, C. 1986. Systematic Software Development Using VDM. Prentice Hall, Hertfordshire, UK."},{"key":"e_1_2_1_14_1","unstructured":"Lopez Pombo C. G. Owre S. and Shankar N. 2002. A Semantic Embedding of the Ag Dynamic Logic in PVS. Tech. Rep. SRI-CSL-02-04 Computer Science Laboratory SRI International. July.  Lopez Pombo C. G. Owre S. and Shankar N. 2002. A Semantic Embedding of the A g Dynamic Logic in PVS. Tech. Rep. SRI-CSL-02-04 Computer Science Laboratory SRI International. July."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_2_1_16_1","volume-title":"Object Constraint Language Specification","author":"Object Management Group","unstructured":"Object Management Group . 1997. Object Constraint Language Specification . Object Management Group , Needham, MA . version 1.1. Object Management Group. 1997. Object Constraint Language Specification. Object Management Group, Needham, MA. version 1.1."},{"key":"e_1_2_1_17_1","unstructured":"Owre S. Shankar N. Rushby J. M. and Stringer-Calvert D. 2001. PVS Language Reference Version 2.4 ed. SRI International.  Owre S. Shankar N. Rushby J. M. and Stringer-Calvert D. 2001. PVS Language Reference Version 2.4 ed. SRI International."},{"key":"e_1_2_1_18_1","volume-title":"Understanding Z: A Specification Language and Its Formal Semantics","author":"Spivey J. M.","unstructured":"Spivey , J. M. 1988. Understanding Z: A Specification Language and Its Formal Semantics . Cambridge University Press , New York, NY . Spivey, J. M. 1988. Understanding Z: A Specification Language and Its Formal Semantics. Cambridge University Press, New York, NY."}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1314493.1314497","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1314493.1314497","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:56:04Z","timestamp":1750254964000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1314493.1314497"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,12]]},"references-count":18,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,12]]}},"alternative-id":["10.1145\/1314493.1314497"],"URL":"https:\/\/doi.org\/10.1145\/1314493.1314497","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,12]]},"assertion":[{"value":"2005-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2007-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2007-12-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}