{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:36:34Z","timestamp":1771025794706,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642287558","type":"print"},{"value":"9783642287565","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28756-5_29","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T16:57:15Z","timestamp":1332435435000},"page":"422-436","source":"Crossref","is-referenced-by-count":11,"title":["A Proof Assistant for Alloy Specifications"],"prefix":"10.1007","author":[{"given":"Mattias","family":"Ulbrich","sequence":"first","affiliation":[]},{"given":"Ulrich","family":"Geilmann","sequence":"additional","affiliation":[]},{"given":"Aboubakr Achraf","family":"El Ghazi","sequence":"additional","affiliation":[]},{"given":"Mana","family":"Taghdiri","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","unstructured":"Abrial, J.-R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: Application to Event-B. Fundamenta Informaticae (2007)"},{"key":"29_CR2","doi-asserted-by":"crossref","unstructured":"Arkoudas, K., Khurshid, S., Marinov, D., Rinard, M.: Integrating model checking and theorem proving for relational reasoning. In: RMICS (2003)","DOI":"10.1007\/978-3-540-24771-5_3"},{"key":"29_CR3","unstructured":"Athena, \n                    \n                      http:\/\/people.csail.mit.edu\/kostas\/dpls\/athena\/"},{"key":"29_CR4","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol.\u00a04334. Springer, Heidelberg (2007)"},{"key":"29_CR5","doi-asserted-by":"crossref","unstructured":"Buss, S.R.: First-order proof theory of arithmetic. In: Handbook of Proof Theory, pp. 79\u2013147. Elsevier (1998)","DOI":"10.1016\/S0049-237X(98)80017-7"},{"key":"29_CR6","unstructured":"van Eijck, J.: Defining (reflexive) transitive closure on finite models, \n                    \n                      http:\/\/homepages.cwi.nl\/~jve\/papers\/08\/pdfs\/FinTransClosRev.pdf"},{"key":"29_CR7","unstructured":"El Ghazi, A.A., Geilmann, U., Ulbrich, M., Taghdiri, M.: A Dual-Engine for Early Analysis of Critical Systems. In: DSCI (2011)"},{"key":"29_CR8","unstructured":"El Ghazi, A.A., Taghdiri, M.: Analyzing Alloy Constraints using an SMT Solver: A Case Study. In: AFM (2010)"},{"key":"29_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-642-21437-0_12","volume-title":"FM 2011: Formal Methods","author":"A.A. Ghazi El","year":"2011","unstructured":"El Ghazi, A.A., Taghdiri, M.: Relational Reasoning via SMT Solving. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 133\u2013148. Springer, Heidelberg (2011)"},{"key":"29_CR10","doi-asserted-by":"crossref","unstructured":"Fortune, S., Leivant, D., O\u2019Donnell, M.: The expressiveness of simple and second-order type structures. J. ACM (1983)","DOI":"10.1145\/322358.322370"},{"key":"29_CR11","doi-asserted-by":"crossref","unstructured":"Frias, M., Pombo, C.G.L.: Interpretability of first-order linear temporal logics in fork algebras. In: Journal of logic and algebraic programming (2006)","DOI":"10.1016\/j.jlap.2005.04.005"},{"key":"29_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-30482-1_19","volume-title":"Formal Methods and Software Engineering","author":"M.F. Frias","year":"2004","unstructured":"Frias, M.F., Pombo, C.G.L., Aguirre, N.M.: An Equational Calculus for Alloy. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 162\u2013175. Springer, Heidelberg (2004)"},{"key":"29_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"678","DOI":"10.1007\/978-3-540-45236-2_37","volume-title":"FME 2003: Formal Methods","author":"M. Frias","year":"2003","unstructured":"Frias, M., Pombo, C.G.L., Baum, G., Aguirre, N.M., Maibaum, T.: Taking Alloy to the movies. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 678\u2013697. Springer, Heidelberg (2003)"},{"key":"29_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"587","DOI":"10.1007\/978-3-540-71209-1_46","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M.F. Frias","year":"2007","unstructured":"Frias, M.F., Pombo, C.G.L., Moscato, M.M.: Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 587\u2013601. Springer, Heidelberg (2007)"},{"key":"29_CR15","doi-asserted-by":"crossref","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen. Mathematische Zeitschrift (1935)","DOI":"10.1007\/BF01201363"},{"key":"29_CR16","unstructured":"Jackson, D.: Software Abstractions: Logic, Language and Analysis. MIT Press (2006)"},{"key":"29_CR17","unstructured":"Jackson, D., Wing, J.: Lightweight formal methods. IEEE Computer (1996)"},{"key":"29_CR18","unstructured":"K\u00f6ker, C.: Discharging Event-B proof obligations. Studienarbeit, Universit\u00e4t Karlsruhe, TH (2008)"},{"key":"29_CR19","doi-asserted-by":"crossref","unstructured":"Lev-Ami, T., Immerman, N., Reps, T.W., Sagiv, M., Srivastava, S., Yorsh, G.: Simulating reachability using first-order logic with applications to verification of linked data structures. Logical Methods in Computer Science\u00a05(2) (2009)","DOI":"10.2168\/LMCS-5(2:12)2009"},{"key":"29_CR20","unstructured":"Shankar, N., Owre, S., Rushby, J., Stringer-Calvert, D.: PVS Prover Guide. Computer Science Laboratory, SRI International (1999)"},{"key":"29_CR21","unstructured":"Ulbrich, M., Geilmann, U., Ghazi, A.A.E., Taghdiri, M.: On proving alloy specifications using KeY. Tech. Rep. 2011-37, Karlsruhe Institute of Technology (2011)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28756-5_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T20:11:11Z","timestamp":1556482271000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28756-5_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642287558","9783642287565"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28756-5_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}