{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:30:47Z","timestamp":1761597047919},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540749691"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74970-7_6","type":"book-chapter","created":{"date-parts":[[2007,10,9]],"date-time":"2007-10-09T23:49:08Z","timestamp":1191973748000},"page":"49-63","source":"Crossref","is-referenced-by-count":10,"title":["Exploring Different Constraint-Based Modelings for Program 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":"6_CR1","unstructured":"A\u00eft-Kaci, H., Berstel, B., Junker, U., Leconte, M., Podelski, A.: Satisfiability Modulo Structures as Constraint Satisfaction: An Introduction. In: Procs. of JFLA, 8 pages (2007)"},{"key":"6_CR2","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, 16 pages (December 19, 2005)","DOI":"10.1007\/11691617_9"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. Clarke","year":"2005","unstructured":"Clarke, E., 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)"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"6_CR6","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\/271771.271790"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Leconte, M., Berstel, B.: Extending a CP Solver with Congruences as Domains for Program Verification. In: Procs. of CSTVA 2006, 1st Workshop on Constraints in Software Testing, Verification and Analysis, Nantes (2006)","DOI":"10.1002\/9780470612309.ch21"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/11691372_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Collavizza","year":"2006","unstructured":"Collavizza, H., Rueher, M.: Software Verification using Constraint Programming Techniques. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 182\u2013196. Springer, Heidelberg (2006)"},{"issue":"4","key":"6_CR9","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., Wegman, M., Zadeck, 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":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. Ganai","year":"2005","unstructured":"Ganai, M., 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":"6_CR11","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proc. of DAC, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT an SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T). Journal of the ACM (to appear)","DOI":"10.1145\/1217856.1217859"},{"key":"6_CR13","volume-title":"Proc of. 16th IEEE International Conference on Automated Software Engineering(ASE 2001)","author":"N.T. Sy","year":"2001","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), IEEE Computer Society Press, Los Alamitos (2001)"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming \u2013 CP 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74970-7_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,18]],"date-time":"2024-02-18T12:11:38Z","timestamp":1708258298000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74970-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540749691"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74970-7_6","relation":{},"subject":[]}}