{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:48:29Z","timestamp":1775868509494,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642327582","type":"print"},{"value":"9783642327599","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32759-9_12","type":"book-chapter","created":{"date-parts":[[2012,8,21]],"date-time":"2012-08-21T06:12:30Z","timestamp":1345529550000},"page":"116-131","source":"Crossref","is-referenced-by-count":7,"title":["A Certified Constraint Solver over Finite Domains"],"prefix":"10.1007","author":[{"given":"Matthieu","family":"Carlier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Catherine","family":"Dubois","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arnaud","family":"Gotlieb","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A modular integration of sat\/smt solvers to coq through proof witnesses. In: Jouannaud, Shao (eds.) [16], pp. 135\u2013150.","DOI":"10.1007\/978-3-642-25379-9_12"},{"issue":"1-2","key":"12_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0004-3702(02)00210-2","volume":"140","author":"F. Bacchus","year":"2002","unstructured":"Bacchus, F., Chen, X., Beek, P., Walsh, T.: Binary vs. non-binary constraints. Artificial Intelligence\u00a0140(1-2), 1\u201337 (2002)","journal-title":"Artificial Intelligence"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-642-29828-8_2","volume-title":"Integration of AI and OR Techniques in Contraint Programming for Combinatorial Optimzation Problems","author":"S. Bardin","year":"2012","unstructured":"Bardin, S., Gotlieb, A.: fdcc: A Combined Approach for Solving Constraints over Finite Domains and Arrays. In: Beldiceanu, N., Jussien, N., Pinson, \u00c9. (eds.) CPAIOR 2012. LNCS, vol.\u00a07298, pp. 17\u201333. Springer, Heidelberg (2012)"},{"issue":"1","key":"12_CR4","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1002\/stvr.423","volume":"21","author":"S. Bardin","year":"2011","unstructured":"Bardin, S., Herrmann, P.: Osmose: Automatic structural testing of executables. Software Testing, Verification and Reliability (STVR)\u00a021(1), 29\u201354 (2011)","journal-title":"Software Testing, Verification and Reliability (STVR)"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-12002-2_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Bardin","year":"2010","unstructured":"Bardin, S., Herrmann, P., Perroud, F.: An Alternative to SAT-Based Approaches for Bit-Vectors. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 84\u201398. Springer, Heidelberg (2010)"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Bessiere, C.: Constraint propagation. In: Handbook of Constraint Programming, ch. 3. Elsevier (2006)","DOI":"10.1016\/S1574-6526(06)80007-6"},{"key":"12_CR7","unstructured":"Besson, F., Cornilleau, P.-E., Pichardie, D.: Modular smt proofs for fast reflexive checking inside coq. In: Jouannaud, Shao (eds.) [16]"},{"key":"12_CR8","unstructured":"B\u00f6hme, S., Fox, A., Sewell, T., Weber, T.: Reconstruction of z3\u2019s bit-vector proofs in hol4 and isabelle\/hol. In: Shao, Jouannaud (eds.) [16]"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-30473-6_5","volume-title":"Tests and Proofs","author":"M. Carlier","year":"2012","unstructured":"Carlier, M., Dubois, C., Gotlieb, A.: A First Step in the Design of a Formally Verified Constraint-Based Testing Tool: FocalTest. In: Brucker, A.D., Julliand, J. (eds.) TAP 2012. LNCS, vol.\u00a07305, pp. 35\u201350. Springer, Heidelberg (2012)"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Bessiere, R.Y.C., R\u00e9gin, J.-C., Zhang, Y.: An optimal coarse-grained arc consistency algorithm. Artificial Intelligence, pp. 165\u2013185 (2005)","DOI":"10.1016\/j.artint.2005.02.004"},{"issue":"2","key":"12_CR11","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/s10601-009-9089-9","volume":"15","author":"H. Collavizza","year":"2010","unstructured":"Collavizza, H., Rueher, M., Van Hentenryck, P.: Cpbpv: A constraint-programming framework for bounded program verification. Constraints Journal\u00a015(2), 238\u2013264 (2010)","journal-title":"Constraints Journal"},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/11691372_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Fontaine","year":"2006","unstructured":"Fontaine, P., Marion, J.-Y., Merz, S., Nieto, L.P., Tiu, A.F.: Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 167\u2013181. Springer, Heidelberg (2006)"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/11589976_3","volume-title":"Integrated Formal Methods","author":"P. Godefroid","year":"2005","unstructured":"Godefroid, P., Klarlund, N.: Software Model Checking: Searching for Computations in the Abstract or the Concrete. In: Romijn, J.M.T., Smith, G.P., van de Pol, J. (eds.) IFM 2005. LNCS, vol.\u00a03771, pp. 20\u201332. Springer, Heidelberg (2005)"},{"key":"12_CR14","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/S0743-1066(98)10006-7","volume":"37","author":"P. Hentenryck Van","year":"1998","unstructured":"Van Hentenryck, P., Saraswat, V., Deville, Y.: Design, implementation, and evaluation of the constraint language cc(fd). JLP\u00a037, 139\u2013164 (1998)","journal-title":"JLP"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Holland, A., O\u2019Sullivan, B.: Robust solutions for combinatorial auctions. In: Riedl, J., Kearns, M.J., Reiter, M.K. (eds.) ACM Conf. on Electronic Commerce (EC 2005), Vancouver, BC, Canada, pp. 183\u2013192 (2005)","DOI":"10.1145\/1064009.1064029"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Certified Programs and Proofs","year":"2011","unstructured":"Jouannaud, J.-P., Shao, Z. (eds.): CPP 2011. LNCS, vol.\u00a07086. Springer, Heidelberg (2011)"},{"issue":"7","key":"12_CR17","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM\u00a052(7), 107\u2013115 (2009)","journal-title":"Communications of the ACM"},{"key":"12_CR18","unstructured":"Lescuyer, S., Conchon, S.: A Reflexive Formalization of a SAT Solver in Coq. In: Emerging Trends of the 21st Int. Conf. on Theorem Proving in Higher Order Logics, TPHOLs (2008)"},{"issue":"1","key":"12_CR19","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. Art. Intel.\u00a08(1), 99\u2013118 (1977)","journal-title":"Art. Intel."},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"McLaughlin, S., Barrett, C., Ge, Y.: Cooperating theorem provers: A case study combining hol-light and cvc lite. ENTCS, vol.\u00a0144(2) (January 2006)","DOI":"10.1016\/j.entcs.2005.12.005"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: POPL 1997, pp. 106\u2013119 (1997)","DOI":"10.1039\/fd106119"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Necula, G.C., Lee, P.: The design and implementation of a certifying compiler. In: PLDI 1998, pp. 333\u2013344 (1998)","DOI":"10.1145\/277652.277752"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Rushby, J.: Verified software: Theories, tools, experiments. In: Automated Test Generation and Verified Software, pp. 161\u2013172. Springer (2008)","DOI":"10.1007\/978-3-540-69149-5_18"}],"container-title":["Lecture Notes in Computer Science","FM 2012: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32759-9_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T21:11:32Z","timestamp":1558300292000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32759-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642327582","9783642327599"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32759-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}