{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T06:17:06Z","timestamp":1725689826132},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642308840"},{"type":"electronic","value":"9783642308857"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30885-7_11","type":"book-chapter","created":{"date-parts":[[2012,6,27]],"date-time":"2012-06-27T08:50:45Z","timestamp":1340787045000},"page":"150-163","source":"Crossref","is-referenced-by-count":17,"title":["Temporal Logic Model Checking in Alloy"],"prefix":"10.1007","author":[{"given":"Amirhossein","family":"Vakili","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nancy A.","family":"Day","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Selic, B.: From Model-Driven Development to Model-Driven Engineering. In: ECRTS. IEEE Computer Society (2007)","DOI":"10.1109\/ECRTS.2007.16"},{"issue":"2","key":"11_CR2","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM TOSEM\u00a011(2), 256\u2013290 (2002)","journal-title":"ACM TOSEM"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: The B\u00a0Book: Assigning Programs to Meanings. Cambridge University Press (August 1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"11_CR4","unstructured":"International Organisation for Standardization: Information Technology Z Formal Specification Notation Syntax, Type System and Semantics (2000)"},{"key":"11_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/11559306_15","volume-title":"Frontiers of Combining Systems","author":"E. B\u00f6rger","year":"2005","unstructured":"B\u00f6rger, E.: The ASM Method for System Design and Analysis. A Tutorial Introduction. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol.\u00a03717, pp. 264\u2013283. Springer, Heidelberg (2005)"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Chang, F.S.H., Jackson, D.: Symbolic Model Checking of Declarative Relational Models. In: ICSE 2006, pp. 312\u2013320 (May 2006)","DOI":"10.1145\/1134285.1134329"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-46419-0_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Castillo Del","year":"2000","unstructured":"Del Castillo, G., Winter, K.: Model Checking Support for the ASM High-Level Language. In: Graf, S. (ed.) TACAS 2000. LNCS, vol.\u00a01785, pp. 331\u2013346. Springer, Heidelberg (2000)"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M. Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 855\u2013874. Springer, Heidelberg (2003)"},{"key":"11_CR9","unstructured":"Jackson, D.: Software Abstractions - Logic, Language, and Analysis. MIT Press (2006)"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/3-540-63166-6_29","volume-title":"Computer Aided Verification","author":"N. Immerman","year":"1997","unstructured":"Immerman, N., Vardi, M.: Model Checking and Transitive-Closure Logic. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 291\u2013302. Springer, Heidelberg (1997)"},{"key":"11_CR11","unstructured":"Clarke, E., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)"},{"key":"11_CR12","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1023\/A:1008615614281","volume":"10","author":"E.M. Clarke","year":"1997","unstructured":"Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another Look at LTL Model Checking. Formal Methods in System Design\u00a010, 47\u201371 (1997)","journal-title":"Formal Methods in System Design"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Hindley, J.R., Seldin, J.P.: An Introduction to Combinators and the \u03bb-calculus, 2nd edn. Cambridge University Press (2008)","DOI":"10.1017\/CBO9780511809835"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: The SMV system (November\u00a006, 1992)","DOI":"10.1007\/978-1-4615-3190-6_4"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 333\u2013336. Springer, Heidelberg (2004)"},{"issue":"4","key":"11_CR16","first-page":"377","volume":"3","author":"G. Schellhorn","year":"1997","unstructured":"Schellhorn, G., Ahrendt, W.: Reasoning about Abstract State Machines: The WAM Case Study. Journal of Universal Computer Science\u00a03(4), 377\u2013413 (1997)","journal-title":"Journal of Universal Computer Science"},{"key":"11_CR17","unstructured":"Dold, A.: A Formal Representation of Abstract State Machines Using PVS. Verifix Technical Report Ulm\/6.2, Universit\u00e4t Ulm (July 1998)"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Frias, M.F., Galeotti, J.P., L\u00f3pez Pombo, C.G., Aguirre, N.M.: DynAlloy: Upgrading Alloy with Actions. In: Proceedings of ICSE 2005, pp. 442\u2013451. ACM (2005)","DOI":"10.1145\/1062455.1062535"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-45309-1_11","volume-title":"Programming Languages and Systems","author":"M. Huth","year":"2001","unstructured":"Huth, M., Jagadeesan, R., Schmidt, D.A.: Modal Transition Systems: A Foundation for Three-Valued Program Analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol.\u00a02028, pp. 155\u2013169. Springer, Heidelberg (2001)"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, VDM, and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30885-7_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T03:06:57Z","timestamp":1606187217000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30885-7_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642308840","9783642308857"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30885-7_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}