{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:31Z","timestamp":1776333451735,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642203978","type":"print"},{"value":"9783642203985","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-20398-5_22","type":"book-chapter","created":{"date-parts":[[2011,4,6]],"date-time":"2011-04-06T19:29:49Z","timestamp":1302118189000},"page":"298-312","source":"Crossref","is-referenced-by-count":56,"title":["Automated Test Case Generation with SMT-Solving and Abstract Interpretation"],"prefix":"10.1007","author":[{"given":"Jan","family":"Peleska","sequence":"first","affiliation":[]},{"given":"Elena","family":"Vorobev","sequence":"additional","affiliation":[]},{"given":"Florian","family":"Lapschies","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","first-page":"69","volume-title":"Proceedings of FMCAD 2009","author":"A. Brillout","year":"2009","unstructured":"Brillout, A., Kroening, D., Wahl, T.: Mixed Abstractions for Floating-Point Arithmetic. In: Proceedings of FMCAD 2009, pp. 69\u201376. IEEE, Los Alamitos (2009)"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Brummayer, R.: Efficient SMT Solving for Bit-Vectors and the Extensional Theory of Arrays. Ph.D. thesis, Johannes Kepler University Linz, Austria (November 2009)","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-540-71209-1_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R.E. Bryant","year":"2007","unstructured":"Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.: Deciding Bit-Vector Arithmetic with Abstraction. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 358\u2013372. Springer, Heidelberg (2007)"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Abstract interpretation: Theory and practice (April 11-13, 2000)","DOI":"10.1145\/325694.325699"},{"key":"22_CR5","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1145\/512950.512973","volume-title":"Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-540-77505-8_23","volume-title":"Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues","author":"P. Cousot","year":"2008","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: Combination of abstractions in the ASTR\u00c9E static analyzer. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol.\u00a04435, pp. 272\u2013300. Springer, Heidelberg (2008)"},{"key":"22_CR7","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809088","volume-title":"Introduction to Lattices and Order","author":"B.A. Davey","year":"2002","unstructured":"Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (2002)"},{"key":"22_CR8","unstructured":"Esterel Technologies: SCADE Suite Product Description, \n                    \n                      http:\/\/www.estereltechnologies.com"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/11814948_25","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"Z. Fu","year":"2006","unstructured":"Fu, Z., Malik, S.: On solving the partial max-sat problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 252\u2013265. Springer, Heidelberg (2006)"},{"issue":"4","key":"22_CR10","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/235321.235322","volume":"5","author":"D. Harel","year":"1996","unstructured":"Harel, D., Naamad, A.: The statemate semantics of statecharts. ACM Transactions on Software Engineering and Methodology\u00a05(4), 293\u2013333 (1996)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Jain, H., Clarke, E.M.: Efficient SAT Solving for Non-Clausal Formulas using DPLL, Graphs, and Watched Cuts. In: 46th Design Automation Conference, DAC (2009)","DOI":"10.1145\/1629911.1630057"},{"key":"22_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0249-6","volume-title":"Applied Interval Analysis","author":"L. Jaulin","year":"2001","unstructured":"Jaulin, L., Kieffer, M., Didrit, O., Walter, \u00c9.: Applied Interval Analysis. Springer, London (2001)"},{"key":"22_CR13","unstructured":"Jung, J., S\u00fclflow, A., Wille, R., Drechsler, R.: SWORD v1.0. Tech. rep. (2009), sMTCOMP 2009: System Description"},{"issue":"6","key":"22_CR14","first-page":"71","volume":"21","author":"S. Ranise","year":"2006","unstructured":"Ranise, S., Tinelli, C.: Satisfiability modulo theories. TRENDS and CONTROVERSIES\u2013IEEE Magazine on Intelligent Systems\u00a021(6), 71\u201381 (2006)","journal-title":"TRENDS and CONTROVERSIES\u2013IEEE Magazine on Intelligent Systems"},{"key":"22_CR15","unstructured":"S\u00f6rensson, N.: MiniSat 2.2 and MiniSat++ 1.1. Tech. rep. (2010), SAT-Race 2010: Solver Descriptions"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Wille, R., Fey, G., Gro\u00dfe, D., Eggersgl\u00fc\u00df, S., Drechsler, R.: SWORD: A SAT like Prover Using Word Level Information. In: Proceedings of VLSI-SoC 2007, pp. 88\u201393 (2007)","DOI":"10.1109\/VLSISOC.2007.4402478"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-20398-5_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T18:34:41Z","timestamp":1558550081000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-20398-5_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642203978","9783642203985"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-20398-5_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}