{"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":1771025794090,"version":"3.50.1"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319175232","type":"print"},{"value":"9783319175249","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17524-9_11","type":"book-chapter","created":{"date-parts":[[2015,4,7]],"date-time":"2015-04-07T06:15:31Z","timestamp":1428387331000},"page":"143-157","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["First-Order Transitive Closure Axiomatization via Iterative Invariant Injections"],"prefix":"10.1007","author":[{"given":"Aboubakr Achraf","family":"El Ghazi","sequence":"first","affiliation":[]},{"given":"Mana","family":"Taghdiri","sequence":"additional","affiliation":[]},{"given":"Mihai","family":"Herda","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,8]]},"reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-24771-5_3","volume-title":"Relational and Kleene-Algebraic Methods in Computer Science","author":"K Arkoudas","year":"2004","unstructured":"Arkoudas, K., Khurshid, S., Marinov, D., Rinard, M.: Integrating model checking and theorem proving for relational reasoning. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) Relational and Kleene-Algebraic Methods in Computer Science. LNCS, vol. 3051, pp. 21\u201333. Springer, Heidelberg (2004)"},{"key":"11_CR2","unstructured":"Barwise, J. (ed.): Handbook of mathematical logic. In: Number 90 in Studies in Logic and the Foundations of Mathematics. North-Holland Publ., Amsterdam (1977)"},{"key":"11_CR3","unstructured":"Best, J.: Proving alloy models by introducing an explicit relational theory in SMT. Studienarbeit, Karlsruhe Institute of Technology, Dec. 2012"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-02959-2_3","volume-title":"Automated Deduction \u2013 CADE-22","author":"MP Bonacina","year":"2009","unstructured":"Bonacina, M.P., Lynch, C., de Moura, L.: On deciding satisfiability by DPLL $$(\\Gamma +{\\cal T})$$ and unsound theorem proving. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 35\u201350. Springer, Heidelberg (2009)"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Dennis, G., Chang, F., Jackson, D.: Modular verification of code with SAT. In: ISSTA, pp. 109\u2013120 (2006)","DOI":"10.1145\/1146238.1146251"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-540-45085-6_22","volume-title":"Automated Deduction \u2013 CADE-19","author":"L Dixon","year":"2003","unstructured":"Dixon, L., Fleuriot, J.D.: IsaPlanner: a prototype proof planner in isabelle. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 279\u2013283. Springer, Heidelberg (2003)"},{"key":"11_CR7","unstructured":"Van Eijck, J.: Defining (reflexive) transitive closure on finite models (2008)"},{"key":"11_CR8","unstructured":"El Ghazi, A.A., Geilmann, U., Ulbrich, M., Taghdiri, M.: A dual-engine for early analysis of critical systems. In: DSCI, Berlin (2011)"},{"key":"11_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":"AA El Ghazi","year":"2011","unstructured":"El Ghazi, A.A., Taghdiri, M.: Relational reasoning via SMT solving. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 133\u2013148. Springer, Heidelberg (2011)"},{"key":"11_CR10","unstructured":"El Ghazi, A.A., Ulbrich, M., Taghdiri, M., Herda, M.: Reducing the complexity of quantified formulas via variable elimination. In: SMT, pp. 87\u201399, July 2013"},{"key":"11_CR11","unstructured":"Enderton, H.B.: A mathematical introduction to logic. Academic Press (1972)"},{"key":"11_CR12","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":"MF 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. 4424, pp. 587\u2013601. Springer, Heidelberg (2007)"},{"issue":"1","key":"11_CR13","first-page":"101","volume":"55","author":"Y Ge","year":"2009","unstructured":"Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. AMAI 55(1), 101\u2013122 (2009)","journal-title":"AMAI"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306\u2013320. Springer, Heidelberg (2009)"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-540-30124-0_15","volume-title":"Computer Science Logic","author":"N Immerman","year":"2004","unstructured":"Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: The boundary between decidability and undecidability for transitive-closure logics. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 160\u2013174. Springer, Heidelberg (2004)"},{"key":"11_CR16","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Apr. 2006"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-87603-8_23","volume-title":"Abstract State Machines, B and Z","author":"E Kang","year":"2008","unstructured":"Kang, E., Jackson, D.: Formal modeling and analysis of a flash filesystem in alloy. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 294\u2013308. Springer, Heidelberg (2008)"},{"key":"11_CR18","volume-title":"Computer-Aided Reasoning: An Approach","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann, M., Strother Moore, J., Manolios, P.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, USA (2000)"},{"key":"11_CR19","unstructured":"Keller, U.: Some remarks on the definability of transitive closure in first-order logic and datalog (2004)"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: ACM SIGPLAN Notices, POPL, pp. 115\u2013126. ACM, New York (2006)","DOI":"10.1145\/1111320.1111048"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/BFb0053570","volume-title":"Programming Languages and Systems","author":"K Rustan","year":"1998","unstructured":"Rustan, K., Leino, M.: Recursive object types in a logic of object-oriented programs. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 170\u2013184. Springer, Heidelberg (1998)"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/11532231_8","volume-title":"Automated Deduction \u2013 CADE-20","author":"T Lev-Ami","year":"2005","unstructured":"Lev-Ami, T., Immerman, N., Reps, T., Sagiv, M., Srivastava, S., Yorsh, G.: Simulating reachability using first-order logic with applications to verification of linked data structures. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 99\u2013115. Springer, Heidelberg (2005)"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Nelson, G.: Verifying reachability invariants of linked structures. In: POPL, pp. 38\u201347, ACM, New York (1983)","DOI":"10.1145\/567067.567073"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39979-7_16","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2003","author":"M Taghdiri","year":"2003","unstructured":"Taghdiri, M., Jackson, D.: A lightweight formal analysis of a multicast key management scheme. In: K\u00f6nig, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol. 2767. Springer, Heidelberg (2003)"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-642-28756-5_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Ulbrich","year":"2012","unstructured":"Ulbrich, M., Geilmann, U., El Ghazi, A.A., Taghdiri, M.: A proof assistant for alloy specifications. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 422\u2013436. Springer, Heidelberg (2012)"},{"key":"11_CR26","unstructured":"Vaziri-Farahani, M.: Finding bugs in software with a constraint solver. Thesis, Massachusetts Institute of Technology (2004)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17524-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,18]],"date-time":"2023-01-18T20:15:57Z","timestamp":1674072957000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17524-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319175232","9783319175249"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17524-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"8 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}