{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T03:50:27Z","timestamp":1760586627535,"version":"3.40.3"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2012,8,30]],"date-time":"2012-08-30T00:00:00Z","timestamp":1346284800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2014,2]]},"DOI":"10.1007\/s10009-012-0258-6","type":"journal-article","created":{"date-parts":[[2012,8,29]],"date-time":"2012-08-29T12:12:05Z","timestamp":1346242325000},"page":"103-121","source":"Crossref","is-referenced-by-count":4,"title":["Constraint-based BMC: a backjumping strategy"],"prefix":"10.1007","volume":"16","author":[{"given":"H\u00e9l\u00e8ne","family":"Collavizza","sequence":"first","affiliation":[]},{"given":"Nguyen","family":"Le Vinh","sequence":"additional","affiliation":[]},{"given":"Olivier","family":"Ponsini","sequence":"additional","affiliation":[]},{"given":"Michel","family":"Rueher","sequence":"additional","affiliation":[]},{"given":"Antoine","family":"Rollet","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,8,30]]},"reference":[{"key":"258_CR1","doi-asserted-by":"crossref","unstructured":"Albert, E., G\u00f3mez-Zamalloa, M., Puebla, G.: Test data generation of bytecode by CLP partial evaluation. In: Logic-Based Program Synthesis and Transformation (LOPSTR), Revised Selected Papers, LNCS, vol. 5438, pp. 4\u201323. Springer, Berlin (2008)","DOI":"10.1007\/978-3-642-00515-2_2"},{"issue":"1","key":"258_CR2","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/s10009-008-0091-0","volume":"11","author":"A Armando","year":"2009","unstructured":"Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using SMT solvers instead of SAT solvers. Int. J. Softw. Tools Technol. Transf. 11(1), 69\u201383 (2009)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"7","key":"258_CR3","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/1965724.1965743","volume":"54","author":"T Ball","year":"2011","unstructured":"Ball, T., Levin, V., Rajami, S.K.: A decade of software model checking with SLAM. CACM 54(7), 68\u201376 (2011)","journal-title":"CACM"},{"issue":"6","key":"258_CR4","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/j.ipl.2004.10.015","volume":"93","author":"M Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. Inf. Process. Lett. 93(6), 281\u2013288 (2005)","journal-title":"Inf. Process. Lett."},{"key":"258_CR5","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without bdds. In: TACAS, pp. 193\u2013207. Springer, Berlin (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"issue":"3","key":"258_CR6","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2010.12.011","volume":"264","author":"B Blanc","year":"2010","unstructured":"Blanc, B., Junke, C., Marre, B., Gall, P.L., Andrieu, O.: Handling state-machines specifications with gatel. MBT 2010. Electr. Notes Theor. Comput. Sci. 264(3), 3\u201317 (2010)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"258_CR7","doi-asserted-by":"crossref","unstructured":"Bochot, T., Virelizier, P., Waeselynck, H., Wiels, V.: Model checking flight control systems: the airbus experience. In: ICSE 2009. 31st International Conference on Software Engineering, Companion Volume, pp. 18\u201327. IEEE, New York (2009)","DOI":"10.1109\/ICSE-COMPANION.2009.5070960"},{"issue":"2","key":"258_CR8","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1002\/stvr.333","volume":"16","author":"B Botella","year":"2006","unstructured":"Botella, B., Gotlieb, A., Michel, C.: Symbolic execution of floating-point computations. Softw. Test. Verif. Reliab. 16(2), 97\u2013121 (2006)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"258_CR9","doi-asserted-by":"crossref","unstructured":"Charreteur, F., Gotlieb, A.: Constraint-based test input generation for java bytecode. In: IEEE 21st International Symposium on Software Reliability Engineering, pp. 131\u2013140. IEEE Computer Society, New York (2010)","DOI":"10.1109\/ISSRE.2010.26"},{"key":"258_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: TACAS, LNCS, vol. 2988, pp. 168\u2013176 (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"258_CR11","doi-asserted-by":"crossref","unstructured":"Collavizza, H., Rueher, M., Hentenryck, P.V.: CPBPV: a constraint-programming framework for bounded program verification. In: CP 2008, 14th International Conference on Principles and Practice of Constraint Programming, LNCS, vol. 5202, pp. 327\u2013341. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-85958-1_22"},{"issue":"2","key":"258_CR12","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/s10601-009-9089-9","volume":"15","author":"H Collavizza","year":"2010","unstructured":"Collavizza, H., Rueher, M., Hentenryck, P.V.: A constraint-programming framework for bounded program verification. Constraints J. 15(2), 238\u2013264 (2010)","journal-title":"Constraints J."},{"key":"258_CR13","unstructured":"Collavizza, H., Vinh, N.L., Rueher, M., Devulder, S., Gueguen, T.: A dynamic constraint-based bmc strategy for generating counterexamples. In: Proceedings of the 2011 ACM Symposium on Applied Computing (SAC), TaiChung, Taiwan, March 21\u201324, 2011, pp. 1633\u20131638. ACM, New York (2011)"},{"key":"258_CR14","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. In: Proceedings of the 24th IEEE\/ACM International Conference on Automated Software Engineering (ASE\u201909), pp. 137\u2013148. IEEE Computer Society, New York (2009)","DOI":"10.1109\/ASE.2009.63"},{"key":"258_CR15","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. ASE 0, 137\u2013148 (2009). http:\/\/doi.ieeecomputersociety.org\/10.1109\/ASE.2009.63"},{"key":"258_CR16","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Feret, J., Min\u00e9, A., Mauborgne, L., Monniaux, D., Rival, X.: Varieties of static analyzers: a comparison with ASTR\u00c9E. In: First Joint IEEE\/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE\u201907), pp. 3\u201320. IEEE Computer Society, New York (2007)","DOI":"10.1109\/TASE.2007.55"},{"issue":"4","key":"258_CR17","doi-asserted-by":"crossref","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.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451\u2013490 (1991)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"258_CR18","doi-asserted-by":"crossref","unstructured":"Delmas, D., Goubault, E., Putot, S., Souyris, J., Tekkal, K., V\u00e9drine, F.: Towards an industrial use of fluctuat on safety-critical avionics software. In: 14th International Workshop on Formal Methods for Industrial Critical Systems (FMICS\u201909), Lecture Notes in Computer Science, vol. 5825, pp. 53\u201369. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-04570-7_6"},{"key":"258_CR19","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201908), LNCS, vol. 4963, pp. 337\u2013340. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"258_CR20","doi-asserted-by":"crossref","unstructured":"Denmat, T., Gotlieb, A., Ducass\u00e9, M.: Improving constraint-based testing with dynamic linear relaxations. In: Proceedings of ISSRE, The 18th IEEE International Symposium on Software, pp. 181\u2013190. IEEE Computer Society, New York (2006)","DOI":"10.1109\/ISSRE.2007.34"},{"key":"258_CR21","unstructured":"D\u2019Silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. CAD Integr. Circuits Syst. 27(7), 1165\u20131178 (2008)"},{"key":"258_CR22","doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Gupta, A.: Accelerating high-level bounded model checking. In: International Conference on Computer-Aided Design (ICCAD\u201906), pp. 794\u2013801 (2006)","DOI":"10.1145\/1233501.1233664"},{"key":"258_CR23","doi-asserted-by":"crossref","unstructured":"Gotlieb, A.: Euclide: a constraint-based testing framework for critical C programs. In: ICST 2009, Second International Conference on Software Testing Verification and Validation, 1\u20134 April 2009, Denver, Colorado, USA, pp. 151\u2013160. IEEE Computer Society, New York (2009)","DOI":"10.1109\/ICST.2009.10"},{"key":"258_CR24","unstructured":"Gotlieb, A.: TCAS software verification using constraint programming (Accepted for publication), The Knowledge Engineering Review (2010)"},{"key":"258_CR25","doi-asserted-by":"crossref","unstructured":"Gotlieb, A., Botella, B., Rueher, M.: Automatic test data generation using constraint solving techniques. In: ISSTA, International Symposium on Software Testing and Analysis, pp. 53\u201362 (1998)","DOI":"10.1145\/271775.271790"},{"key":"258_CR26","doi-asserted-by":"crossref","unstructured":"Jackson, D., Vazir, M.: Finding bugs with a constraint solver. In: ISSTA, International Symposium on Software Testing and Analysis, pp. 14\u201325. ACM Press, New York (2000)","DOI":"10.1145\/347636.383378"},{"key":"258_CR27","doi-asserted-by":"crossref","unstructured":"Marre, B., Arnould, A.: Test sequences generation from lustre descriptions: Gatel. ASE press, New York (2000)","DOI":"10.1109\/ASE.2000.873667"},{"key":"258_CR28","doi-asserted-by":"crossref","unstructured":"Michel, L., Hentenryck, P.V.: The comet programming language and system. In: van Beek, P. (ed.) Proceedings of the 11th International Conference on Principles and Practice of Constraint Programming (CP\u201905), LNCS, vol. 3709, pp. 881\u2013881. Springer, Berlin (2005)","DOI":"10.1007\/11564751_119"},{"key":"258_CR29","unstructured":"Nguyen, L.V., Collavizza, H., Rueher, M., Devulder, S., Gueguen, T.: Strat\u00e9gies dynamiques pour la g\u00e9n\u00e9ration de contre-exemples. In: Actes des Sixi\u00e8mes Journ\u00e9es Francophones de Programmation par Contraintes (JFPC\u20192010), pp. 207\u2013216 (2010)"},{"key":"258_CR30","unstructured":"R\u00e9gin, J.C.: A filtering algorithm for constraints of difference in csps. In: AAAI, pp. 362\u2013367 (1994)"},{"key":"258_CR31","unstructured":"Rossi, F., van Beek, P., Walsh, T. (eds.): Handbook of Constraint Programming. Elsevier, Amsterdam (2006)"},{"key":"258_CR32","doi-asserted-by":"crossref","unstructured":"Sy, N.T., Deville, Y.: Automatic test data generation for programs with integer and float variables. In: ASE (16th IEEE International Conference on Automated Software Engineering), pp. 13\u201321. IEEE Computer Society, New York (2001)","DOI":"10.1109\/ASE.2001.989786"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0258-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-012-0258-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0258-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T12:42:38Z","timestamp":1744029758000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-012-0258-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8,30]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["258"],"URL":"https:\/\/doi.org\/10.1007\/s10009-012-0258-6","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2012,8,30]]}}}