{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T04:42:34Z","timestamp":1773808954037,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540330561","type":"print"},{"value":"9783540330578","type":"electronic"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"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":[[2006]]},"DOI":"10.1007\/11691372_12","type":"book-chapter","created":{"date-parts":[[2006,3,28]],"date-time":"2006-03-28T09:22:26Z","timestamp":1143537746000},"page":"182-196","source":"Crossref","is-referenced-by-count":21,"title":["Exploration of the Capabilities of Constraint Programming for Software Verification"],"prefix":"10.1007","author":[{"given":"H\u00e9l\u00e8ne","family":"Collavizza","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michel","family":"Rueher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Armando, A., Mantovani, J., Platania, L.: Bounded Model Checking of C Programs using a SMT solver instead of a SAT solver Technical Report, AI-Lab, DIST, University of Genova, December 19, 16 pages (2005)","DOI":"10.1007\/11691617_9"},{"key":"12_CR2","unstructured":"Ball, T., Rajamani, S.K.: Boolean Programs: A Model and Process For Software Analysis. Technical Report MSR TR 200-14 (2000)"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/978-3-540-31980-1_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Bouquet","year":"2005","unstructured":"Bouquet, F., Dadeau, F., Legeard, B., Utting, M.: JML-Testing-Tools: a Symbolic Animator for JML Specifications using CLP. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 551\u2013556. Springer, Heidelberg (2005)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroenig, D., Lerda, F.: A Tool for Checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"12_CR5","first-page":"105","volume-title":"Formal Methods in System Design","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroenig, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSIC Programs using SAT. In: Formal Methods in System Design, vol.\u00a025, pp. 105\u2013127. Kluwer Academic Press, Dordrecht (2004)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1007\/978-3-540-31980-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.M. Clarke","year":"2005","unstructured":"Clarke, E.M., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-Based Predicate Abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 570\u2013574. Springer, Heidelberg (2005)"},{"issue":"2","key":"12_CR7","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1145\/151257.151258","volume":"2","author":"R.A. Demillo","year":"1993","unstructured":"Demillo, R.A., Offut, A.J.: Experimental Results from an Automatic Test Case Generator. ACM Transactions on Software Engineering Methodology\u00a02(2), 109\u2013175 (1993)","journal-title":"ACM Transactions on Software Engineering Methodology"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast Decision Procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Gotlieb, A., Botella, B., Rueher, M.: Automatic Test Data Generation using Constraint Solving Techniques. In: Proc. ISSTA 1998, ACM SIGSOFT, vol.\u00a02, pp. 53\u201362 (1998)","DOI":"10.1145\/271775.271790"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Gotlieb, A., Botella, B., Rueher, M.: A CLP Framework for Computing Structural Test Data. In: Proc of Computational Logic (CL 2000), pp. 399-413 (2000)","DOI":"10.1007\/3-540-44957-4_27"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"563","DOI":"10.1007\/978-3-540-31980-1_39","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C.W. Keller","year":"2005","unstructured":"Keller, C.W., Saha, D., Basu, S., Smolka, S.A.: FocusCheck: A tool for model checking and debugging sequential C programs. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 563\u2013569. Springer, Heidelberg (2005)"},{"key":"12_CR12","doi-asserted-by":"publisher","first-page":"642","DOI":"10.1016\/S0140-3664(99)00223-6","volume":"23","author":"O. Kon","year":"2000","unstructured":"Kon, O., Castanet, R.: Test generation for interworking systems. Computer Communications\u00a023, 642\u2013652 (2000)","journal-title":"Computer Communications"},{"key":"12_CR13","volume-title":"Apt: Principles of Constraint Programming","author":"R. Krzystof","year":"2003","unstructured":"Krzystof, R.: Apt: Principles of Constraint Programming. Cambridge University Press, Cambridge (2003)"},{"issue":"4","key":"12_CR14","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R. Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficently Computing Static Single Assignment Form and the Control Dependence Graph. Transactions on Programming Languages and Systems\u00a013(4), 451\u2013490 (1991)","journal-title":"Transactions on Programming Languages and Systems"},{"key":"12_CR15","unstructured":"Leavens Gary, T.: Cheon Yoonsik: Design by Contract with JML (August 2005), \n                    \n                      http:\/\/www.jmlspecs.org"},{"issue":"1","key":"12_CR16","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/0004-3702(77)90007-8","volume":"8","author":"A. Mackworth","year":"1977","unstructured":"Mackworth, A.: Consistency in networks of relations. Journal of Artificial Intelligence\u00a08(1), 99\u2013118 (1977)","journal-title":"Journal of Artificial Intelligence"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1007\/978-3-540-31980-1_41","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M.K. Ganai","year":"2005","unstructured":"Ganai, M.K., Gupta, A., Ashar, P.: DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 575\u2013580. Springer, Heidelberg (2005)"},{"key":"12_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8917-8","volume-title":"Constraint and integer programming","author":"M. Milano","year":"2004","unstructured":"Milano, M.: Constraint and integer programming. Kluwer Academic Publisher, Dordrecht (2004)"},{"key":"12_CR19","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0020-0255(74)90008-5","volume":"7","author":"U. Montanari","year":"1974","unstructured":"Montanari, U.: Networks of constraints: Fundamental properties and applications to image processing. Information science\u00a07, 95\u2013132 (1974)","journal-title":"Information science"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: M: Chaff: Engineering an Efficient SAT Solver. In: Proc of DAC, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"12_CR21","volume-title":"Constraint Processing","author":"R. Dechter","year":"2003","unstructured":"Dechter, R.: Constraint Processing. Morgan Kaufmann, San Francisco (2003)"},{"key":"12_CR22","unstructured":"Sy, N.T., Deville, Y.: Automatic test data generation for programs with integer and float variables. In: Proc. of. 16th IEEE International Conference on Automated Software Engineering, ASE 2001 (2001)"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Sy, N.T., Deville, Y.: Consistency Techniques for interprocedural Test Data Generation. In: Proc. of the Joint 9th European Software Engineering Conference and 11th ACM SIGSOFT Symposium on the Foundation of Software Engineering (ESEC\/FSE 2003), Helsinki, Finland (2003)","DOI":"10.1145\/940071.940087"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11691372_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:33:20Z","timestamp":1558272800000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11691372_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540330561","9783540330578"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/11691372_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}