{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,24]],"date-time":"2025-03-24T07:34:55Z","timestamp":1742801695326},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2015,3,27]],"date-time":"2015-03-27T00:00:00Z","timestamp":1427414400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Electron Test"],"published-print":{"date-parts":[[2015,4]]},"DOI":"10.1007\/s10836-015-5518-4","type":"journal-article","created":{"date-parts":[[2015,3,26]],"date-time":"2015-03-26T14:12:15Z","timestamp":1427379135000},"page":"151-166","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Scalable and Optimized Hybrid Verification of Embedded Software"],"prefix":"10.1007","volume":"31","author":[{"given":"J\u00f6rg","family":"Behrend","sequence":"first","affiliation":[]},{"given":"Djones","family":"Lettnin","sequence":"additional","affiliation":[]},{"given":"Alexander","family":"Gr\u00fcnhage","sequence":"additional","affiliation":[]},{"given":"J\u00fcrgen","family":"Ruf","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Kropf","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Rosenstiel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,3,27]]},"reference":[{"key":"5518_CR1","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1145\/381694.378846","volume":"36","author":"T Ball","year":"2001","unstructured":"Ball T, Majumdar R, Millstein T, Rajamani SK (2001) Automatic predicate abstraction of C programs. SIGPLAN Not 36:203\u2013213","journal-title":"SIGPLAN Not"},{"key":"5518_CR2","unstructured":"Barrett C, Sebastiani R, Seshia SA, Tinelli C (2009) Satisfiability modulo theories, ser. Frontiers in artificial intelligence and applications, vol 185, ch. 26. IOS Press, pp 825\u2013885"},{"key":"5518_CR3","doi-asserted-by":"crossref","unstructured":"Behrend J, Lettnin D, Heckler P, Ruf J, Kropf T, Rosenstiel W (2011) Scalable hybrid verification for embedded software. In: DATE \u201911: Proceedings of the conference on design, automation and test in Europe, pp 1\u20136","DOI":"10.1109\/DATE.2011.5763039"},{"key":"5518_CR4","doi-asserted-by":"crossref","unstructured":"Beyer D, Henzinger TA, Jhala R, Majumdar R (2007) The software model checker BLAST: applications to software engineering. Int J Softw Tools Technol Transfer","DOI":"10.1007\/s10009-007-0044-z"},{"key":"5518_CR5","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke EM, Strichman O, Zhu Y (2003) Bounded model checking. In: Zelkowitz M (ed) Highly dependable software, ser. Advances in computers, vol 58. Academic Press","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"5518_CR6","first-page":"322","volume-title":"Exe: automatically generating inputs of death. In: Proceedings of the 13th ACM Conference on Computer and Communications Security, ser. CCS \u201906","author":"C Cadar","year":"2006","unstructured":"Cadar C, Ganesh V, Pawlowski PM, Dill DL, Engler DR (2006) Exe: automatically generating inputs of death. In: Proceedings of the 13th ACM conference on computer and communications security, ser. CCS \u201906. ACM, New York, pp 322\u2013335. doi: 10.1145\/1180405.1180445"},{"key":"5518_CR7","first-page":"209","volume-title":"KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX conference on operating systems design and implementation, ser. OSDI\u201908","author":"C Cadar","year":"2008","unstructured":"Cadar C, Dunbar D, Engler D (2008) KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX conference on operating systems design and implementation, ser. OSDI\u201908. USENIX Association, Berkeley, pp 209\u2013224"},{"issue":"5","key":"5518_CR8","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E Clarke","year":"1994","unstructured":"Clarke E, Grumberg O, Long D (1994) Model checking and abstraction. ACM Trans Program Lang Syst 16(5):1512\u20131542","journal-title":"ACM Trans Program Lang Syst"},{"key":"5518_CR9","first-page":"415","volume-title":"Conference on computer aided verification (CAV), ser. Lecture Notes in Computer Science, vol 818","author":"E Clarke","year":"1994","unstructured":"Clarke E, Grumberg O, Hamaguchi K (1994) Another look at LTL model checking. In: Dill DL (ed) Conference on computer aided verification (CAV), ser. Lecture Notes in Computer Science, vol 818. Springer, Stanford, pp 415\u2013427"},{"key":"5518_CR10","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2003) Counterexample-guided abstraction refinement for symbolic model checking. J ACM 50:752\u2013794","journal-title":"J ACM"},{"key":"5518_CR11","doi-asserted-by":"crossref","first-page":"368","DOI":"10.21236\/ADA461052","volume-title":"Behavioral consistency of C and verilog programs using bounded model checking. In: Proceedings of the 40th annual design automation conference, DAC \u201903","author":"E Clarke","year":"2003","unstructured":"Clarke E, Kroening D, Yorav K (2003) Behavioral consistency of C and verilog programs using bounded model checking. In: Proceedings of the 40th annual design automation conference, DAC \u201903. ACM, New York, pp 368\u2013371"},{"key":"5518_CR12","doi-asserted-by":"crossref","unstructured":"Clarke E, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: In tools and algorithms for the construction and analysis of systems. Springer, pp 168\u2013176","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"5518_CR13","doi-asserted-by":"crossref","unstructured":"Clarke E, Kroening D, Sharygina N, Yorav K (2005) SATABS: SAT-based predicate abstraction for ANSI-C. In: TACAS, 3440. Springer, pp 570\u2013574","DOI":"10.1007\/978-3-540-31980-1_40"},{"key":"5518_CR14","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1109\/ASE.2009.63","volume-title":"SMT-based bounded model checking for embedded ANSI-C software. In: Proceedings of the 2009 IEEE\/ACM international conference on automated software engineering, ASE \u201909","author":"L Cordeiro","year":"2009","unstructured":"Cordeiro L, Fischer B, Marques-Silva J (2009) SMT-based bounded model checking for embedded ANSI-C software. In: Proceedings of the 2009 IEEE\/ACM international conference on automated software engineering, ASE \u201909. IEEE Computer Society, Washington, pp 137\u2013148"},{"key":"5518_CR15","doi-asserted-by":"crossref","unstructured":"Cordeiro L, Fischer B, Chen H, Marques-Silva J (2009) Semiformal verification of embedded software in medical devices considering stringent hardware constraints. Second Int Conf Embed Softw Syst:396\u2013403","DOI":"10.1109\/ICESS.2009.82"},{"key":"5518_CR16","first-page":"108","volume-title":"Formal methods for industrial critical systems, ser. Lecture Notes in Computer Science, vol 7437","author":"L Correnson","year":"2012","unstructured":"Correnson L, Signoles J (2012) Combining analyses for C program verification. In: Stoelinga M, Pinger R (eds), Formal methods for industrial critical systems, ser. Lecture Notes in Computer Science, vol 7437. Springer, Berlin, pp 108\u2013130"},{"key":"5518_CR17","first-page":"233","volume-title":"Frama-c: a software analysis perspective. In: Proceedings of the 10th international conference on software engineering and formal methods, ser. SEFM\u201912","author":"P Cuoq","year":"2012","unstructured":"Cuoq P, Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B (2012) Frama-c: a software analysis perspective. In: Proceedings of the 10th international conference on software engineering and formal methods, ser. SEFM\u201912. Springer, Berlin, pp 233\u2013247"},{"key":"5518_CR18","doi-asserted-by":"crossref","unstructured":"Di Guglielmo G, Fummi F, Pravadelli G, Soffia S, Roveri M (2010) Semi-formal functional verification by EFSM traversing via NuSMV. In: High level design validation and test workshop (HLDVT), 2010 IEEE International, pp 58\u201365","DOI":"10.1109\/HLDVT.2010.5496660"},{"key":"5518_CR19","doi-asserted-by":"crossref","unstructured":"Di Guglielmo G, Fujita M, Fummi F, Pravadelli G, Soffia S (2011) EFSM-based model-driven approach to concolic testing of system-level design. In: 2011 9th IEEE\/ACM international conference on formal methods and models for codesign (MEMOCODE). pp 201\u2013209","DOI":"10.1109\/MEMCOD.2011.5970527"},{"key":"5518_CR20","doi-asserted-by":"crossref","unstructured":"Edwards SA, Ma T, Damiano R (2001) Using a hardware model checker to verify software. In: Proceedings of the 4th international conference on ASIC (ASICON)","DOI":"10.1109\/ICASIC.2001.982504"},{"key":"5518_CR21","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1145\/565816.503291","volume":"37","author":"C Flanagan","year":"2002","unstructured":"Flanagan C, Qadeer S (2002) Predicate abstraction for software verification. SIGPLAN Not 37:191\u2013202","journal-title":"SIGPLAN Not"},{"key":"5518_CR22","unstructured":"GNU (2010) Gcov coverage. [Online]. Available: http:\/\/gcc.gnu.org\/onlinedocs\/gcc\/Gcov.html"},{"issue":"6","key":"5518_CR23","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1145\/1064978.1065036","volume":"40","author":"P Godefroid","year":"2005","unstructured":"Godefroid P, Klarlund N, Sen K (2005) Dart: directed automated random testing. SIGPLAN Not 40 (6):213\u2013223. doi: 10.1145\/1064978.1065036","journal-title":"SIGPLAN Not"},{"key":"5518_CR24","doi-asserted-by":"crossref","first-page":"731","DOI":"10.1145\/1146909.1147096","volume-title":"Directed-simulation assisted formal verification of serial protocol and bridge. In: DAC \u201906: Proceedings of the 43rd annual Design Automation Conference","author":"S Gorai","year":"2006","unstructured":"Gorai S, Biswas S, Bhatia L, Tiwari P, Mitra RS (2006) Directed-simulation assisted formal verification of serial protocol and bridge. In: Proceedings of the 43rd annual design automation conference, DAC \u201906. ACM, New York , pp 731\u2013736"},{"key":"5518_CR25","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/11537328_4","volume":"3639","author":"TA Henzinger","year":"2005","unstructured":"Henzinger TA, Jhala R, Majumdar R (2005) The BLAST software verification system. Model Checking Softw 3639:25\u201326","journal-title":"Model Checking Softw"},{"key":"5518_CR26","doi-asserted-by":"crossref","DOI":"10.1007\/b105739","volume-title":"Embedded Software for SoC","author":"AA Jerraya","year":"2003","unstructured":"Jerraya AA, Yoo S, Verkest D, Wehn N (2003) Embedded Software for SoC. Kluwer Academic Publishers, Norwell"},{"key":"5518_CR27","doi-asserted-by":"crossref","unstructured":"Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B (2015) Frama-c: a software analysis perspective. Form Asp Comput:1\u201337","DOI":"10.1007\/s00165-014-0326-7"},{"key":"5518_CR28","unstructured":"Kroening D (2009) Bounded model checking for ANSI-C. [Online]. Available: http:\/\/www.cprover.org\/cbmc\/"},{"key":"5518_CR29","first-page":"15","volume-title":"Languages and compilers for high performance computing, ser. Lecture notes in computer science, vol 3602","author":"C Lattner","year":"2005","unstructured":"Lattner C, Adve V (2005) The llvm compiler framework and infrastructure tutorial. In: Eigenmann R, Li Z, Midkiff S (eds) Languages and compilers for high performance computing, ser. Lecture notes in computer science, vol 3602. Springer, Berlin, pp 15\u201316"},{"key":"5518_CR30","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1145\/1403375.1403417","volume-title":"Verification of temporal properties in automotive embedded software. In: DATE \u201908: proceedings of the conference on design, automation and test in Europe","author":"D Lettnin","year":"2008","unstructured":"Lettnin D, Nalla PK, Ruf J, Kropf T, Rosenstiel W, Kirsten T, Sch\u00f6nknecht V, Reitemeyer S (2008) Verification of temporal properties in automotive embedded software. In: DATE \u201908: proceedings of the conference on design, automation and test in Europe. ACM, New York , pp 164\u2013169"},{"key":"5518_CR31","doi-asserted-by":"crossref","unstructured":"Lettnin D, Nalla PK, Behrend J, Ruf J, Gerlach J, Kropf T, Rosenstiel W, Sch\u00f6nknecht V, Reitemeyer S (2009) Semiformal verification of temporal properties in automotive hardware dependent software. In: DATE \u201909: Proceedings of the conference on design, automation and test in Europe, pp 1214\u20131217","DOI":"10.1109\/DATE.2009.5090847"},{"key":"5518_CR32","doi-asserted-by":"crossref","unstructured":"Malik A, Moyer B, Cermak D (2000) The M\u2019CORE(TM) M340 Unified Cache Architecture. In: Proceedings of the 2000 international conference on computer design. pp 577\u2013580","DOI":"10.1109\/ICCD.2000.878347"},{"key":"5518_CR33","unstructured":"MISRA MISRA - The Motor Industry Software Reliability Association,\u201d 2000. [Online]. Available: http:\/\/www.misra.org.uk\/"},{"key":"5518_CR34","doi-asserted-by":"crossref","first-page":"737","DOI":"10.1145\/1146909.1147097","volume-title":"Guiding simulation with increasingly refined abstract traces. In: DAC \u201906: Proceedings of the 43rd annual Design Automation Conference","author":"K Nanshi","year":"2006","unstructured":"Nanshi K, Somenzi F (2006) Guiding simulation with increasingly refined abstract traces. In: DAC \u201906: Proceedings of the 43rd annual Design Automation Conference. ACM, New York , pp 737\u2013742"},{"key":"5518_CR35","doi-asserted-by":"crossref","unstructured":"Necula GC, McPeak S, Rahul SP, Weimer W (2002) CIL: intermediate language and tools for analysis and transformation of C programs. Comput Complex:213\u2013228","DOI":"10.1007\/3-540-45937-5_16"},{"key":"5518_CR36","unstructured":"NEC NEC Electronics (Europe) GmbH http:\/\/www.eu.necel.com\/"},{"key":"5518_CR37","unstructured":"Open SystemC Initiative (2003) SystemC Verification Standard Library 1.0p Users Manual"},{"key":"5518_CR38","unstructured":"Ruf J., Peranandam PM, Kropf T, Rosenstiel W (2003) Bounded property checking with symbolic simulation. In: FDL"},{"issue":"5","key":"5518_CR39","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1145\/1095430.1081750","volume":"30","author":"K Sen","year":"2005","unstructured":"Sen K, Marinov D, Agha G (2005) CUTE: a concolic unit testing engine for C. SIGSOFT Softw Eng Notes 30(5):263\u2013272. doi: 10.1145\/1095430.1081750","journal-title":"SIGSOFT Softw Eng Notes"},{"key":"5518_CR40","unstructured":"Shea R Call graph visualization for C and TinyOS programs, Dept. of Computer Science School of Engineering UCLA, 2009. [Online]. Available: http:\/\/www.ambleramble.org\/callgraph\/index.html"},{"key":"5518_CR41","first-page":"134","volume-title":"Proceedings of the 2Nd international conference on tests and proofs, ser. TAP\u201908","author":"N Tillmann","year":"2008","unstructured":"Tillmann N, De Halleux J (2008) Pex: White box test generation for.net. In: Proceedings of the 2Nd international conference on tests and proofs, ser. TAP\u201908. [Online]. Available: http:\/\/dl.acm.org\/citation.cfm?id=1792786.1792798 . Springer, Berlin, pp 134\u2013153"},{"key":"5518_CR42","unstructured":"Weiss RJ, Ruf J, Kropf T, Rosenstiel W (2005) Efficient and customizable integration of temporal properties into SystemC. Forum on specification & Design Languages (FDL):271\u2013282"}],"container-title":["Journal of Electronic Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-015-5518-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10836-015-5518-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-015-5518-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,22]],"date-time":"2019-08-22T08:47:45Z","timestamp":1566463665000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10836-015-5518-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,27]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,4]]}},"alternative-id":["5518"],"URL":"https:\/\/doi.org\/10.1007\/s10836-015-5518-4","relation":{},"ISSN":["0923-8174","1573-0727"],"issn-type":[{"value":"0923-8174","type":"print"},{"value":"1573-0727","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3,27]]}}}