{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,23]],"date-time":"2025-03-23T04:23:40Z","timestamp":1742703820197,"version":"3.40.2"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2012,3,11]],"date-time":"2012-03-11T00:00:00Z","timestamp":1331424000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2012,8]]},"DOI":"10.1007\/s10009-012-0227-0","type":"journal-article","created":{"date-parts":[[2012,3,10]],"date-time":"2012-03-10T20:46:43Z","timestamp":1331412403000},"page":"439-459","source":"Crossref","is-referenced-by-count":1,"title":["Model generation for quantified formulas with application to test data generation"],"prefix":"10.1007","volume":"14","author":[{"given":"Christoph D.","family":"Gladisch","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,3,11]]},"reference":[{"key":"227_CR1","doi-asserted-by":"crossref","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) Proceedings, Computer Aided Verification, 19th International Conference, CAV 2007, LNCS, vol. 4590, pp. 298\u2013302. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73368-3_34"},{"issue":"1","key":"227_CR2","doi-asserted-by":"crossref","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. Int. J. Artif. Intell. Tools 15(1), 21\u201352 (2006)","journal-title":"Int. J. Artif. Intell. Tools"},{"volume-title":"Verification of Object-Oriented Software: The KeY Approach, LNCS, vol. 4334","year":"2007","key":"227_CR3","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds): Verification of Object-Oriented Software: The KeY Approach, LNCS, vol. 4334. Springer, Berlin (2007)"},{"key":"227_CR4","doi-asserted-by":"crossref","unstructured":"Benhamou, F., Goualard, F.: Universally quantified interval constraints. In: Dechter, R. (eds.) Principles and Practice of Constraint Programming-CP 2000, 6th International Conference, Singapore, LNCS, vol. 1894, pp. 67\u201382. Springer, Berlin (2000)","DOI":"10.1007\/3-540-45349-0_7"},{"key":"227_CR5","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) Proceedings, Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, vol. 3855, pp. 427\u2013442. Springer, Berlin (2006)","DOI":"10.1007\/11609773_28"},{"key":"227_CR6","doi-asserted-by":"crossref","unstructured":"Csallner, C., Smaragdakis, Y.: Check \u2018n\u2019 Crash: combining static checking and testing. In: ICSE, pp. 422\u2013431. ACM, New York (2005)","DOI":"10.1145\/1062455.1062533"},{"key":"227_CR7","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Engineering DPLL(T) + saturation. In: IJCAR, LNCS, vol. 5195, pp. 475\u2013490. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-71070-7_40"},{"key":"227_CR8","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, LNCS, vol. 4963, pp. 337\u2013340. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"3","key":"227_CR9","doi-asserted-by":"crossref","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 11(3), 255\u2013260 (2009)","journal-title":"STTT"},{"key":"227_CR10","doi-asserted-by":"crossref","unstructured":"Deng, X., Robby, Hatcliff, J.: Kiasan\/KUnit: Automatic test case generation and analysis feedback for open object-oriented systems. In: TAICPART-MUTATION \u201907: Proceedings of the Testing: Academic and Industrial Conference Practice and Research Techniques\u2014MUTATION, pp. 3\u201312. IEEE Computer Society, Washington, DC (2007)","DOI":"10.1109\/TAIC.PART.2007.32"},{"issue":"3","key":"227_CR11","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs D., Nelson G., Saxe J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"227_CR12","doi-asserted-by":"crossref","unstructured":"du Bousquet, L., Ledru, Y., Maury, O., Oriat, C., Lanet, J.-L.: Case study in jml-based software validation. In: ASE, pp. 294\u2013297. IEEE CS (2004)","DOI":"10.1109\/ASE.2004.1342750"},{"key":"227_CR13","unstructured":"Dutertre, B., de Moura, L.: The Yices SMT solver. Technical report, Computer Science Laboratory, SRI International, 2006. http:\/\/yices.csl.sri.com\/tool-paper.pdf . (2010)"},{"key":"227_CR14","doi-asserted-by":"crossref","unstructured":"Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) Proceedings, Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, LNCS, vol. 4144, pp. 81\u201394. Springer, Berlin (2006)","DOI":"10.1007\/11817963_11"},{"key":"227_CR15","unstructured":"Engel, C.: Verification based test case generation. Master\u2019s thesis, University of Karlsruhe, Institut f\u00fcr Theoretische Informatik (2006)"},{"key":"227_CR16","doi-asserted-by":"crossref","unstructured":"Engel, C., Gladisch, C., Klebanov, V., R\u00fcmmer, P.: Integrating verification and testing of object-oriented software. In: Beckert, B., H\u00e4hnle, R. (eds.) Proceedings, Tests and Proofs, Second International Conference, TAP 2008, Prato, LNCS, vol. 4966, pp. 182\u2013191. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-79124-9_13"},{"issue":"1\u20132","key":"227_CR17","doi-asserted-by":"crossref","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. 55(1\u20132), 101\u2013122 (2009)","journal-title":"Ann. Math. Artif. Intell."},{"key":"227_CR18","doi-asserted-by":"crossref","unstructured":"Ge, Y., de Moura, L.M.: Complete instantiation for quantified formulas in satisfiability modulo theories. In: Bouajjani, A., Maler, O. (eds.) Proceedings, Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, LNCS, vol. 5643, pp. 306\u2013320. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"227_CR19","unstructured":"Gent, I.P., Nightingale, P., Stergiou, K.: QCSP-Solve: a solver for quantified constraint satisfaction problems. In: Kaelbling, L.P., Saffiotti, A. (eds.) Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, Edinburgh (IJCAI 2005), pp. 138\u2013143. Professional Book Center (2005)"},{"issue":"1","key":"227_CR20","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1016\/S1571-0661(04)80650-9","volume":"86","author":"S. Ghilardi","year":"2003","unstructured":"Ghilardi S.: Quantifier elimination and provers integration. Electr. Notes Theor. Comput. Sci. 86(1), 22\u201334 (2003)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"227_CR21","unstructured":"Giese, M.: Incremental closure of free variable tableaux. In: Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) Proceedings, Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, LNCS, vol. 2083, pp. 545\u2013560. Springer, Berlin (2001)"},{"key":"227_CR22","doi-asserted-by":"crossref","unstructured":"Gladisch, C.: Verification-based test case generation for full feasible branch coverage. In: Cerone, A., Gruner, S. (eds.) Proceedings, Sixth IEEE International Conference on Software Engineering and Formal Methods, SEFM 2008, Cape Town, pp. 159\u2013168. IEEE Computer Society (2008)","DOI":"10.1109\/SEFM.2008.22"},{"key":"227_CR23","doi-asserted-by":"crossref","unstructured":"Gladisch, C.: Could we have chosen a better loop invariant or method contract? In: Dubois, C. (eds.) Proceedings, Tests and Proofs, Third International Conference, TAP 2009, Zurich, LNCS, vol. 5668, pp. 74\u201389. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02949-3_7"},{"key":"227_CR24","doi-asserted-by":"crossref","unstructured":"Gladisch, C.: Satisfiability solving and model generation for quantified first-order logic formulas. In: Beckert, B., March\u00e9, C. (eds.) Conf. Post. Proc., Formal Verification of Object-Oriented Software International Conference, FoVeOOS 2010, Paris, LNCS, vol. 6528. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-18070-5_6"},{"key":"227_CR25","doi-asserted-by":"crossref","unstructured":"Gladisch, C.: Test data generation for programs with quantified first-order logic specifications. In: Petrenko, A., da Silva Sim\u00e3o A., Maldonado, J.C. (eds.) Proceedings, Testing Software and Systems\u201422nd IFIP WG 6.1 International Conference, ICTSS 2010, Natal, LNCS, vol. 6435, pp. 158\u2013173. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-16573-3_12"},{"key":"227_CR26","unstructured":"Gladisch, C.: Verification-Based Software-Fault Detection. PhD thesis, Karlsruhe Institute of Technology (KIT), Karlsruhe (2011)"},{"key":"227_CR27","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. MIT Press, London (2000)"},{"key":"227_CR28","unstructured":"KeY project homepage. http:\/\/www.key-project.org\/ . Accessed 8 Mar 2012"},{"key":"227_CR29","doi-asserted-by":"crossref","unstructured":"Kiniry, J.R., Morkan, A.E., Denby, B.: Soundness and completeness warnings in ESC\/Java2. In: Proceedings of Fifth International Workshop Specification and Verification of Component-Based Systems, pp. 19\u201324 (2006)","DOI":"10.1145\/1181195.1181200"},{"key":"227_CR30","unstructured":"Leavens, G., Cheon, Y.: Design by contract with JML, 2006. http:\/\/www.eecs.ucf.edu\/leavens\/JML\/\/jmldbc.pdf . Visited December (2010)"},{"issue":"2","key":"227_CR31","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1002\/stvr.294","volume":"14","author":"P. McMinn","year":"2004","unstructured":"McMinn P.: Search-based software test data generation: a survey. Softw. Test. Verif. Reliab. 14(2), 105\u2013156 (2004)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"227_CR32","unstructured":"Moskal, M.: Satisfiability Modulo Software. PhD thesis, University of Wroc\u0142aw (2009)"},{"issue":"2","key":"227_CR33","doi-asserted-by":"crossref","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. 198(2), 19\u201335 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"227_CR34","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Challenges in satisfiability modulo theories. In: Baader, F. (eds.) Term Rewriting and Applications, 18th International Conference, RTA 2007, Paris, France, LNCS, vol. 4533, pp. 2\u201318. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73449-9_2"},{"key":"227_CR35","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Handbook of Automated Reasoning, pp. 371\u2013443. Elsevier, MIT Press, London (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"227_CR36","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer, P.: Sequential, parallel, and quantified updates of first-order structures. In: LPAR, LNCS, vol. 4246, pp. 422\u2013436. Springer, Berlin (2006)","DOI":"10.1007\/11916277_29"},{"key":"227_CR37","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer, P., Shah, M.A.: Proving programs incorrect using a sequent calculus for Java dynamic logic. In: Gurevich, Y., Meyer, B. (eds) Proceedings, Tests and Proofs, First International Conference, TAP 2007, LNCS, vol. 4454, pp. 41\u201360. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73770-4_3"},{"key":"227_CR38","doi-asserted-by":"crossref","unstructured":"Visser, W., P\u01ces\u01cereanu, C., Khurshid, S.: Test input generation with Java PathFinder. In: ISSTA, pp. 97\u2013107. ACM, New York (2004)","DOI":"10.1145\/1013886.1007526"},{"key":"227_CR39","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: Spass version 3.5. In: CADE, LNCS, vol. 5663, pp. 140\u2013145. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02959-2_10"},{"key":"227_CR40","doi-asserted-by":"crossref","unstructured":"Zhang, J., Zhang, H.: Extending finite model searching with congruence closure computation. In: Buchberger, B., Campbell, J.A. (eds.) Proceedings, Artificial Intelligence and Symbolic Computation, 7th International Conference, AISC 2004, Linz, LNCS, vol. 3249, pp. 94\u2013102. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-30210-0_9"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0227-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-012-0227-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0227-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T23:17:06Z","timestamp":1742685426000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-012-0227-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,11]]},"references-count":40,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["227"],"URL":"https:\/\/doi.org\/10.1007\/s10009-012-0227-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2012,3,11]]}}}