{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,13]],"date-time":"2026-04-13T19:43:06Z","timestamp":1776109386645,"version":"3.50.1"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2010,4,29]],"date-time":"2010-04-29T00:00:00Z","timestamp":1272499200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2010,12]]},"DOI":"10.1007\/s10817-010-9172-3","type":"journal-article","created":{"date-parts":[[2010,4,28]],"date-time":"2010-04-28T05:59:53Z","timestamp":1272434393000},"page":"397-414","source":"Crossref","is-referenced-by-count":22,"title":["Using Bounded Model Checking for Coverage Analysis of Safety-Critical Software in an Industrial Setting"],"prefix":"10.1007","volume":"45","author":[{"given":"Damiano","family":"Angeletti","sequence":"first","affiliation":[]},{"given":"Enrico","family":"Giunchiglia","sequence":"additional","affiliation":[]},{"given":"Massimo","family":"Narizzano","sequence":"additional","affiliation":[]},{"given":"Alessandra","family":"Puddu","sequence":"additional","affiliation":[]},{"given":"Salvatore","family":"Sabina","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,4,29]]},"reference":[{"key":"9172_CR1","doi-asserted-by":"crossref","unstructured":"Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating Tests from Counterexamples. In: ICSE, pp. 326\u2013335. IEEE Computer Society (2004)","DOI":"10.1109\/ICSE.2004.1317455"},{"key":"9172_CR2","first-page":"118","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 118\u2013149 (2003)","journal-title":"Adv. Comput."},{"key":"9172_CR3","first-page":"193","volume-title":"TACAS. Lecture Notes in Computer Science, vol. 1579","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, R. (ed.) TACAS. Lecture Notes in Computer Science, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999)","edition":"1579"},{"key":"9172_CR4","doi-asserted-by":"crossref","unstructured":"Black, P.E., Ammann, P., Ding, W., N.\u00a0I. of\u00a0Standards, T. (U.S.): Model checkers in software testing. U.S. Dept. of Commerce, Technology Administration, National Institute of Standards and Technology, Gaithersburg (2002)","DOI":"10.6028\/NIST.IR.6777"},{"key":"9172_CR5","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Draves, R., van Renesse, R. (eds.) OSDI, pp. 209\u2013224. USENIX Association (2008)"},{"key":"9172_CR6","first-page":"66","volume-title":"Computer aided verification. 13th international conference, CAV 2001, Paris, France, 18\u201322 July 2001, Proceedings. Lecture Notes in Computer Science, vol. 2102","author":"H Chockler","year":"2001","unstructured":"Chockler, H., Kupferman, O., Kurshan, R.P., Vardi, M.Y.: A practical approach to coverage in model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) Computer aided verification. 13th international conference, CAV 2001, Paris, France, 18\u201322 July 2001, Proceedings. Lecture Notes in Computer Science, vol. 2102, pp. 66\u201378. Springer, Heidelberg (2001)","edition":"2102"},{"key":"9172_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Kroening, D., Ouaknine, J., Strichman, O.: Completeness and Complexity of Bounded Model Checking. In: Steffen, B., Levi, G. (eds.) VMCAI. Lecture Notes in Computer Science, vol. 2937, pp. 85\u201396. Springer (2004)","DOI":"10.1007\/978-3-540-24622-0_9"},{"key":"9172_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Kroening, D., Yorav, K.: Behavioral consistency of C and verilog programs using bounded model checking. In: DAC, pp. 368\u2013371. ACM (2003)","DOI":"10.21236\/ADA461052"},{"key":"9172_CR9","volume-title":"Machine Intelligence, vol. 7","author":"D Cooper","year":"1972","unstructured":"Cooper, D.: Theorem proving in arithmetic without multiplication. In: Meltzer, B., Michie, D. (eds) Machine Intelligence, vol. 7. Edinburgh University Press, Edinburgh (1972)"},{"key":"9172_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1007\/3-540-44585-4_43","volume-title":"Computer aided verification. 13th international conference, CAV 2001, Paris, France, 18\u201322 July 2001, Proceedings","author":"F Copty","year":"2001","unstructured":"Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.Y.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) Computer aided verification. 13th international conference, CAV 2001, Paris, France, 18\u201322 July 2001, Proceedings. Lecture Notes in Computer Science, vol. 2102, pp. 436\u2013453. Springer, Heidelberg (2001)"},{"issue":"4","key":"9172_CR11","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":"9172_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-540-79124-9_12","volume-title":"Tests and proofs, second international conference, TAP 2008, Prato, Italy, 9\u201311 April 2008. Proceedings.","author":"J Halleux de","year":"2008","unstructured":"de\u00a0Halleux, J., Tillmann, N.: Parameterized unit testing with Pex. In: Beckert, B., H\u00e4hnle, R. (eds.) Tests and proofs, second international conference, TAP 2008, Prato, Italy, 9\u201311 April 2008. Proceedings. In: Lecture Notes in Computer Science, vol. 4966, pp. 171\u2013181. Springer, Heidelberg (2008)"},{"key":"9172_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"TACAS.","author":"LM Moura de","year":"2008","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R. Rehof, J. (eds.) TACAS. Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"1","key":"9172_CR14","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1109\/69.75894","volume":"3","author":"WH Deason","year":"1991","unstructured":"Deason, W.H., Brown, D.B., Chang, K.-H., Cross, J.H.: A rule-based software test data generator. IEEE Trans. Knowl. Data Eng. 3(1), 108\u2013117 (1991)","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"9172_CR15","unstructured":"EC: European committee for electrotechnical standardization. In: Railway Applications\u2014Communication, Signalling and Processing Systems - Software for Railway Control and Protection Systems (2008)"},{"key":"9172_CR16","unstructured":"Edvardsson, J.: A survey on automatic test data generation. In: Proceedings of the Second Conference on Computer Science and Engineering in Link\u00f6ping. pp. 21\u201328 (1999)"},{"key":"9172_CR17","series-title":"Lecture Notes in Computer Science","first-page":"502","volume-title":"SAT","author":"N E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT. Lecture Notes in Computer Science, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2003)"},{"key":"9172_CR18","unstructured":"ERTMS: The official Website: http:\/\/www.ertms.com\/"},{"issue":"1","key":"9172_CR19","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1145\/226155.226158","volume":"5","author":"R Ferguson","year":"1996","unstructured":"Ferguson, R., Korel, B.: The chaining approach for software test data generation. ACM Trans. Softw. Eng. Methodol. 5(1), 63\u201386 (1996)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"9172_CR20","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1145\/1065010.1065036","volume-title":"PLDI","author":"P Godefroid","year":"2005","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Sarkar, V., Hall, M.W. (eds.) PLDI, pp. 213\u2013223. ACM (2005)"},{"key":"9172_CR21","doi-asserted-by":"crossref","unstructured":"Jackson, D., Shlyakhter, I., Sridharan, M.: A micromodularity mechanism. In: ESEC\/SIGSOFT FSE, pp. 62\u201373 (2001)","DOI":"10.1145\/503209.503219"},{"issue":"4","key":"9172_CR22","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1023\/B:AUSE.0000038938.10589.b9","volume":"11","author":"S Khurshid","year":"2004","unstructured":"Khurshid, S., Marinov, D.: TestEra: specification-based testing of java programs using SAT. Autom. Softw. Eng. 11(4), 403\u2013434 (2004)","journal-title":"Autom. Softw. Eng."},{"issue":"2","key":"9172_CR23","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1002\/stvr.225","volume":"11","author":"C Meudec","year":"2001","unstructured":"Meudec, C.: ATGen: automatic test data generation using constraint logic programming and symbolic execution. Softw. Test., Verif. Reliab. 11(2), 81\u201396 (2001)","journal-title":"Softw. Test., Verif. Reliab"},{"key":"9172_CR24","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: DAC, pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"key":"9172_CR25","doi-asserted-by":"crossref","unstructured":"Offutt, A.J., Hayes, J.H.: A semantic model of program faults. In: ISSTA, pp. 195\u2013200 (1996)","DOI":"10.1145\/226295.226317"},{"issue":"3","key":"9172_CR26","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"DA Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2(3), 293\u2013304 (1986)","journal-title":"J. Symb. Comput."},{"key":"9172_CR27","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 263\u2013272 (2005)","DOI":"10.1145\/1081706.1081750"},{"key":"9172_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/978-3-540-79124-9_10","volume-title":"Tests and proofs, second international conference, TAP 2008, Prato, Italy, 9\u201311 April 2008. Proceedings","author":"N Tillmann","year":"2008","unstructured":"Tillmann, N., de\u00a0Halleux, J.: Pex-White box test generation for .NET. In: Beckert, B., H\u00e4hnle, R. (eds.) Tests and proofs, second international conference, TAP 2008, Prato, Italy, 9\u201311 April 2008. Proceedings. In: Lecture Notes in Computer Science, vol. 4966, pp. 134\u2013153. Springer, Heidelberg (2008)","edition":"4966"},{"key":"9172_CR29","doi-asserted-by":"crossref","unstructured":"Tillmann, N., Schulte, W.: Parameterized unit tests. In: Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 253\u2013262 (2005)","DOI":"10.1145\/1081706.1081749"},{"key":"9172_CR30","doi-asserted-by":"crossref","unstructured":"Tracey, N., Clark, J.A., Mander, K.: Automated program flaw finding using simulated annealing. In: ISSTA, pp. 73\u201381 (1998)","DOI":"10.1145\/271771.271792"},{"key":"9172_CR31","unstructured":"Vedula, V.M., Abraham, J.A., Ambler, T.P., Aziz, A., Chase, C.M., Tupuri, R.S., Vedula, M.A., Tech, B.: HDL slicing for verification and test (2003)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9172-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-010-9172-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9172-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,31]],"date-time":"2023-05-31T22:45:59Z","timestamp":1685573159000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-010-9172-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,4,29]]},"references-count":31,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2010,12]]}},"alternative-id":["9172"],"URL":"https:\/\/doi.org\/10.1007\/s10817-010-9172-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,4,29]]}}}