{"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":1771025794780,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642214363","type":"print"},{"value":"9783642214370","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21437-0_12","type":"book-chapter","created":{"date-parts":[[2011,6,18]],"date-time":"2011-06-18T03:33:16Z","timestamp":1308367996000},"page":"133-148","source":"Crossref","is-referenced-by-count":22,"title":["Relational Reasoning via SMT Solving"],"prefix":"10.1007","author":[{"given":"Aboubakr Achraf","family":"El Ghazi","sequence":"first","affiliation":[]},{"given":"Mana","family":"Taghdiri","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"The Alloy community, http:\/\/alloy.mit.edu\/community\/"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, A., Rabinovich, A., Sagiv, M.: Decidable fragments of many-sorted logic. Preprint submitted to Elsevier (2009)","DOI":"10.1016\/j.jsc.2009.03.003"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Arkoudas, K., Khurshid, S., Marinov, D., Rinard, M.: Integrating model checking and theorem proving for relational reasoning. In: RELMICS, pp. 21\u201333 (2003)","DOI":"10.1007\/978-3-540-24771-5_3"},{"key":"12_CR4","unstructured":"The satisfiability modulo theories library, http:\/\/goedel.cs.uiowa.edu\/smtib"},{"key":"12_CR5","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":"M.P. Bonacina","year":"2009","unstructured":"Bonacina, M.P., Lynch, C., de Moura, L.: On deciding satisfiability by dPLL( $\\Gamma+{\\mathcal T}$ ) and unsound theorem proving. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 35\u201350. Springer, Heidelberg (2009)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bjorner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"12_CR7","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":"12_CR8","unstructured":"Dutertre, B., de Moura, L.: The Yices SMT Solver. Tool Document (2006)"},{"key":"12_CR9","unstructured":"Erk\u00f6k, L., Matthews, J.: Using Yices as an automated solver in Isabelle\/HOL. In: AFM (2008)"},{"key":"12_CR10","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)"},{"issue":"1","key":"12_CR11","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\u00a055(1), 101\u2013122 (2009)","journal-title":"AMAI"},{"key":"12_CR12","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., Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 306\u2013320. Springer, Heidelberg (2009)"},{"key":"12_CR13","unstructured":"EI Ghazi, A.A., Taghdiri, M.: Analyzing Alloy constraints using an SMT solver: A case study. In: AFM, Edinburgh, United Kingdom (2010)"},{"key":"12_CR14","volume-title":"Software Abstractions: Logic, Lang. and Analysis","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Lang. and Analysis. MIT Press, Cambridge (2006)"},{"key":"12_CR15","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.\u00a05238, pp. 294\u2013308. Springer, Heidelberg (2008)"},{"key":"12_CR16","unstructured":"Khurshid, S.: Generating Structurally Complex Tests from Declarative Constraints. PhD thesis, MIT (2003)"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Khurshid, S., Jackson, D.: Exploring the design of an intentional naming scheme with an automatic constraint analyzer. In: ASE (2000)","DOI":"10.1109\/ASE.2000.873646"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Leino, R., Monahan, R.: Reasoning about comprehensions with first-order SMT solvers. In: SAC, pp. 615\u2013622 (2009)","DOI":"10.1145\/1529282.1529411"},{"key":"12_CR19","series-title":"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., et al.: Simulating reachability using first-order logic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 99\u2013115. Springer, Heidelberg (2005)"},{"key":"12_CR20","unstructured":"Nolte, T.: Exploring filesystem synchronization with lightweight modeling and analysis. Master\u2019s thesis, MIT (2002)"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Owre, S., Shankar, N., Rushby, J.: PVS: A prototype verification system. In: CADE-11 (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"key":"12_CR22","unstructured":"Spass: Automated prover for FOL with equality, http:\/\/www.spass-prover.org\/"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/978-3-642-18275-4_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Suter","year":"2011","unstructured":"Suter, P., Steiger, R., Kuncak, V.: Sets with cardinality constraints in satisfiability modulo theories. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 403\u2013418. Springer, Heidelberg (2011)"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","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.\u00a02767, pp. 240\u2013256. Springer, Heidelberg (2003)"},{"issue":"1","key":"12_CR25","first-page":"87","volume":"14","author":"M. Taghdiri","year":"2007","unstructured":"Taghdiri, M., Jackson, D.: Inferring specifications to detect errors in code. JASE\u00a014(1), 87\u2013121 (2007)","journal-title":"JASE"},{"key":"12_CR26","unstructured":"Torlak, E.: A Constraint Solver for Software Engineering. PhD thesis, MIT (2009)"},{"key":"12_CR27","unstructured":"Vaziri, M.: Finding Bugs in Software with Constraint Solver. PhD thesis (2004)"}],"container-title":["Lecture Notes in Computer Science","FM 2011: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21437-0_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T20:07:22Z","timestamp":1560283642000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21437-0_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642214363","9783642214370"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21437-0_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}