{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:21:48Z","timestamp":1725574908252},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642180699"},{"type":"electronic","value":"9783642180705"}],"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-18070-5_6","type":"book-chapter","created":{"date-parts":[[2011,1,15]],"date-time":"2011-01-15T09:18:02Z","timestamp":1295083082000},"page":"76-91","source":"Crossref","is-referenced-by-count":1,"title":["Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas"],"prefix":"10.1007","author":[{"given":"Christoph D.","family":"Gladisch","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2007","unstructured":"Barrett, C.W., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"issue":"1","key":"6_CR2","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1142\/S0218213006002552","volume":"15","author":"P. Baumgartner","year":"2006","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the model evolution calculus. International Journal on Artificial Intelligence Tools\u00a015(1), 21\u201352 (2006)","journal-title":"International Journal on Artificial Intelligence Tools"},{"key":"6_CR3","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":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-45349-0_7","volume-title":"Principles and Practice of Constraint Programming - CP 2000","author":"F. Benhamou","year":"2000","unstructured":"Benhamou, F., Goualard, F.: Universally quantified interval constraints. In: Dechter, R. (ed.) CP 2000. LNCS, vol.\u00a01894, pp. 67\u201382. Springer, Heidelberg (2000)"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-642-13977-2_11","volume-title":"Tests and Proofs","author":"J.C. Blanchette","year":"2010","unstructured":"Blanchette, J.C.: Relational analysis of (co)inductive predicates (co)algebraic datatypes, and (co)recursive functions. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol.\u00a06143, pp. 117\u2013134. Springer, Heidelberg (2010)"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 427\u2013442. Springer, Heidelberg (2005)"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"6_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","volume-title":"Automated Deduction \u2013 CADE-21","author":"L. Moura de","year":"2007","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 183\u2013198. Springer, Heidelberg (2007)"},{"key":"6_CR9","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., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"3","key":"6_CR10","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/s10009-009-0105-6","volume":"11","author":"D. D\u00e9harbe","year":"2009","unstructured":"D\u00e9harbe, D., Ranise, S.: Satisfiability solving for software verification. STTT\u00a011(3), 255\u2013260 (2009)","journal-title":"STTT"},{"key":"6_CR11","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report. J. ACM (2003)"},{"key":"6_CR12","unstructured":"Dutertre, B., de Moura, L.: The YICES SMT solver. Technical report, Computer Science Laboratory, SRI International (2006)"},{"issue":"1-2","key":"6_CR13","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/s10472-009-9153-6","volume":"55","author":"Y. Ge","year":"2009","unstructured":"Ge, Y., Barrett, C.W., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. Ann. Math. Artif. Intell.\u00a055(1-2), 101\u2013122 (2009)","journal-title":"Ann. Math. Artif. Intell."},{"key":"6_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.M.: 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":"6_CR15","doi-asserted-by":"crossref","unstructured":"Ghilardi, S.: Quantifier elimination and provers integration. Electr. Notes Theor. Comput. Sci.\u00a086(1) (2003)","DOI":"10.1016\/S1571-0661(04)80650-9"},{"key":"6_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/3-540-45744-5_46","volume-title":"Automated Reasoning","author":"M. Giese","year":"2001","unstructured":"Giese, M.: Incremental closure of free variable tableaux. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 545\u2013560. Springer, Heidelberg (2001)"},{"key":"6_CR17","unstructured":"Gladisch, C.: Satisfiability solving and model generation for quantified first-order logic formulas. Karlsruhe Reports in Informatics, Fakult\u00e4t f\u00fcr Informatik Institut f\u00fcr Theoretische Informatik, ITI (2010) ISSN: 2190-4782"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-642-16573-3_12","volume-title":"Testing Software and Systems","author":"C. Gladisch","year":"2010","unstructured":"Gladisch, C.: Test data generation for programs with quantified first-order logic specifications. In: Petrenko, A., Sim\u00e3o, A., Maldonado, J.C. (eds.) ICTSS 2010. LNCS, vol.\u00a06435, pp. 158\u2013173. Springer, Heidelberg (2010)"},{"key":"6_CR19","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D. Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. The MIT Press, London (2000)"},{"key":"6_CR20","unstructured":"KeY project homepage, http:\/\/www.key-project.org\/"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Kiniry, J.R., Morkan, A.E., Denby, B.: Soundness and completeness warnings in ESC\/Java2. In: Proc. Fifth Int. Workshop Specification and Verification of Component-Based Systems, pp. 19\u201324 (2006)","DOI":"10.1145\/1181195.1181200"},{"key":"6_CR22","unstructured":"Moskal, M.: Satisfiability Modulo Software. PhD thesis, University of Wroc\u0142aw (2009)"},{"issue":"2","key":"6_CR23","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.entcs.2008.04.078","volume":"198","author":"M. Moskal","year":"2008","unstructured":"Moskal, M., Lopuszanski, J., Kiniry, J.R.: E-matching for fun and profit. Electr. Notes Theor. Comput. Sci.\u00a0198(2), 19\u201335 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-73449-9_2","volume-title":"Term Rewriting and Applications","author":"R. Nieuwenhuis","year":"2007","unstructured":"Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Challenges in satisfiability modulo theories. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533, pp. 2\u201318. Springer, Heidelberg (2007)"},{"key":"6_CR25","series-title":"Applied Logic Series","volume-title":"Automated Model Building","author":"C. Ricardo","year":"2004","unstructured":"Ricardo, C., Alexander, L., Nicolas, P.: Automated Model Building. Applied Logic Series, vol.\u00a031. Springer, Heidelberg (2004)"},{"key":"6_CR26","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/11916277_29","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. R\u00fcmmer","year":"2006","unstructured":"R\u00fcmmer, P.: Sequential, parallel, and quantified updates of first-order structures. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 422\u2013436. Springer, Heidelberg (2006)"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-540-73770-4_3","volume-title":"Tests and Proofs","author":"P. R\u00fcmmer","year":"2007","unstructured":"R\u00fcmmer, P., Shah, M.A.: Proving programs incorrect using a sequent calculus for java dynamic logic. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol.\u00a04454, pp. 41\u201360. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Formal Verification of Object-Oriented Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-18070-5_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T18:09:10Z","timestamp":1559930950000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-18070-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642180699","9783642180705"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-18070-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}