{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:13:31Z","timestamp":1725549211691},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642120015"},{"type":"electronic","value":"9783642120022"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12002-2_7","type":"book-chapter","created":{"date-parts":[[2010,3,8]],"date-time":"2010-03-08T01:20:25Z","timestamp":1268011225000},"page":"84-98","source":"Crossref","is-referenced-by-count":15,"title":["An Alternative to SAT-Based Approaches for Bit-Vectors"],"prefix":"10.1007","author":[{"given":"S\u00e9bastien","family":"Bardin","sequence":"first","affiliation":[]},{"given":"Philippe","family":"Herrmann","sequence":"additional","affiliation":[]},{"given":"Florian","family":"Perroud","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","volume-title":"Constraint Logic Programming using Eclipse","author":"K.R. Apt","year":"2007","unstructured":"Apt, K.R., Wallace, M.: Constraint Logic Programming using Eclipse. Cambridge University Press, New York (2007)"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"TACAS 2009","author":"R. Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 174\u2013177. Springer, Heidelberg (2009)"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-70545-1_28","volume-title":"Computer Aided Verification","author":"R. Bruttomesso","year":"2008","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: The MathSAT 4 SMT Solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 299\u2013303. Springer, Heidelberg (2008)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"569","DOI":"10.1007\/3-540-36577-X_41","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Barray","year":"2003","unstructured":"Barray, F., Codognet, P., Diaz, D., Michel, H.: Code-based test generation for validation of functional processor descriptions. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 569\u2013584. Springer, Heidelberg (2003)"},{"key":"7_CR6","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1109\/ICST.2008.8","volume-title":"1st Int.\u00a0 Conf.\u00a0 on Software Testing, Verification, and Validation","author":"S. Bardin","year":"2008","unstructured":"Bardin, S., Herrmann, P.: Structural Testing of Executables. In: 1st Int.\u00a0 Conf.\u00a0 on Software Testing, Verification, and Validation, pp. 22\u201331. IEEE Computer Society, Los Alamitos (2008)"},{"key":"7_CR7","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1145\/512950.512973","volume-title":"4th ACM 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: 4th ACM Symposium on Principles of Programming Languages, pp. 238\u2013252. ACM, New York (1977)"},{"key":"7_CR8","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1145\/1180405.1180445","volume-title":"13th ACM Conf.\u00a0 on Computer and Communications Security","author":"C. Cadar","year":"2006","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: automatically generating inputs of death. In: 13th ACM Conf.\u00a0 on Computer and Communications Security, pp. 322\u2013335. ACM, New York (2006)"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.M. Clarke","year":"2004","unstructured":"Clarke, E.M., Kroening, 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":"7_CR10","unstructured":"Diaz, D., Codognet, P.: Design and Implementation of the GNU Prolog System. J.\u00a0Functional and Logic Programming, 2001. EAPLS (2001)"},{"key":"7_CR11","volume-title":"Constraint Processing","author":"R. Dechter","year":"2003","unstructured":"Dechter, R.: Constraint Processing. Morgan Kaufmann, San Francisco (2003)"},{"key":"7_CR12","first-page":"744","volume-title":"5th Conf. on Design, Automation and Test in Europe","author":"F. Ferrandi","year":"2002","unstructured":"Ferrandi, F., Rendine, M., Sciuto, D.: Functional verification for SystemC descriptions using constraint solving. In: 5th Conf. on Design, Automation and Test in Europe, pp. 744\u2013751. IEEE Computer Society, Los Alamitos (2002)"},{"issue":"1-3","key":"7_CR13","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/S0743-1066(98)10005-5","volume":"37","author":"T. Fr\u00fchwirth","year":"1998","unstructured":"Fr\u00fchwirth, T.: Theory and Practice of Constraint Handling Rules. J.\u00a0Logic Programming\u00a037(1-3), 95\u2013138 (1998)","journal-title":"J.\u00a0Logic Programming"},{"key":"7_CR14","first-page":"226","volume-title":"10th Int. ACM SIGPLAN Conf. on Principles and Practice of Declarative Programming","author":"T. Feydy","year":"2008","unstructured":"Feydy, T., Schutt, A., Stuckey, P.J.: Global difference constraint propagation for finite domain solvers. In: 10th Int. ACM SIGPLAN Conf. on Principles and Practice of Declarative Programming, pp. 226\u2013236. ACM, New York (2008)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V. Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.L.: A Decision Procedure for Bit-Vectors and Arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 519\u2013531. Springer, Heidelberg (2007)"},{"key":"7_CR16","unstructured":"Jussien, N., Rochart, G., Lorca, X.: The CHOCO constraint programming solver. In: CPAIOR 2008 Workshop on Open-Source Software for Integer and Contraint Programming (2008)"},{"key":"7_CR17","volume-title":"Decision Procedures: An Algorithmic Point of View.","author":"D. Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Springer, Heidelberg (2008)"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Leconte, M., Berstel, B.: Extending a CP Solver With Congruences as Domains for Software Verification. In: CP 2006 Workshop on Constraints in Software Testing, Verification and Analysis (2006)","DOI":"10.1002\/9780470612309.ch21"},{"key":"7_CR19","unstructured":"Lecoutre, C., Tabary, S.: Abscon 112: Toward more Robustness. In CSP Solver Competition, held with CP 2008 (2008)"},{"key":"7_CR20","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/j.entcs.2004.12.010","volume":"111","author":"B. Marre","year":"2005","unstructured":"Marre, B., Blanc, B.: Test selection strategies for Lustre descriptions in GATeL. Electr.\u00a0Notes Theor.\u00a0Comput.\u00a0Sci.\u00a0111, 93\u2013111 (2005)","journal-title":"Electr.\u00a0Notes Theor.\u00a0Comput.\u00a0Sci."},{"key":"7_CR21","first-page":"530","volume-title":"38th Design Automation Conf.","author":"M. Moskewicz","year":"2001","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: 38th Design Automation Conf., pp. 530\u2013535. ACM, New York (2001)"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-540-72788-0_3","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"P. Manolios","year":"2007","unstructured":"Manolios, P., Vroon, D.: Efficient circuit to CNF conversion. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 4\u20139. Springer, Heidelberg (2007)"},{"key":"7_CR23","first-page":"31","volume-title":"8th IEEE Workshop on RTL and High Level Testing","author":"A. S\u00fclflow","year":"2007","unstructured":"S\u00fclflow, A., K\u00fchne, U., Wille, R., Gro\u00dfe, D., Drechsler, R.: Evaluation of SAT like proof techniques for formal verification of word level circuits. In: 8th IEEE Workshop on RTL and High Level Testing, pp. 31\u201336. IEEE Computer Society, Los Alamitos (2007)"},{"key":"7_CR24","unstructured":"SMT competition, http:\/\/www.smtcomp.org\/"},{"issue":"2","key":"7_CR25","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1109\/92.386221","volume":"3","author":"R. Vemuri","year":"1995","unstructured":"Vemuri, R., Kalyanaraman, R.: Generation of design verification tests from behavioral VHDL programs using path enumeration and constraint programming. IEEE Transactions on VLSI Systems\u00a03(2), 201\u2013214 (1995)","journal-title":"IEEE Transactions on VLSI Systems"},{"key":"7_CR26","first-page":"88","volume-title":"18th Int.\u00a0Conf.\u00a0on Very Large Scale Integration of Systems-on-Chip","author":"R. Wille","year":"2007","unstructured":"Wille, R., Fey, G., Gro\u00dfe, D., Eggersgl\u00fc\u00df, S., Drechsler, R.: SWORD: A SAT like prover using word level information. In: 18th Int.\u00a0Conf.\u00a0on Very Large Scale Integration of Systems-on-Chip, pp. 88\u201393. IEEE, Los Alamitos (2007)"},{"key":"7_CR27","first-page":"375","volume-title":"11th Int.\u00a0Conf.\u00a0on Very Large Scale Integration of Systems-on-Chip","author":"Z. Zeng","year":"2001","unstructured":"Zeng, Z., Ciesielski, M., Rouzeyre, B.: Functional test generation using Constraint Logic Programming. In: 11th Int.\u00a0Conf.\u00a0on Very Large Scale Integration of Systems-on-Chip, pp. 375\u2013387. Kluwer, Dordrecht (2001)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12002-2_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,24]],"date-time":"2024-03-24T18:07:41Z","timestamp":1711303661000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12002-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642120015","9783642120022"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12002-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}