{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T20:32:06Z","timestamp":1768163526038,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642324680","type":"print"},{"value":"9783642324697","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":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32469-7_14","type":"book-chapter","created":{"date-parts":[[2012,8,21]],"date-time":"2012-08-21T21:07:27Z","timestamp":1345583247000},"page":"207-221","source":"Crossref","is-referenced-by-count":21,"title":["Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution"],"prefix":"10.1007","author":[{"given":"Ji\u0159\u00ed","family":"Slab\u00fd","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Strej\u010dek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marek","family":"Trt\u00edk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-540-78800-3_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Anand","year":"2008","unstructured":"Anand, S., Godefroid, P., Tillmann, N.: Demand-Driven Compositional Symbolic Execution. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 367\u2013381. Springer, Heidelberg (2008)"},{"key":"14_CR2","unstructured":"Andersen, L.O.: Program analysis and specialization for the C programming language. PhD thesis, DIKU, University of Copenhagen, report 94\/19 (1994)"},{"key":"14_CR3","unstructured":"Ball, T., Bounimova, E., Kumar, R., Levin, V.: SLAM2: Static driver verification with under 4% false alarms. In: Proceedings of FMCAD, pp. 35\u201342. IEEE (2010)"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with SLAM. Journal on Commun. ACM\u00a054(7) (2011)","DOI":"10.1145\/1965724.1965743"},{"issue":"5","key":"14_CR5","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker BLAST. Journal on Software Tools for Technology Transfer\u00a09(5), 505\u2013525 (2007)","journal-title":"Journal on Software Tools for Technology Transfer"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Binkley, D.W., Gallanger, K.B.: Program slicing. Advances in Computers\u00a043 (1996)","DOI":"10.1016\/S0065-2458(08)60641-5"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-642-00768-2_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N. Bj\u00f8rner","year":"2009","unstructured":"Bj\u00f8rner, N., Tillmann, N., Voronkov, A.: Path Feasibility Analysis for String-Manipulating Programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 307\u2013321. Springer, Heidelberg (2009)"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-540-78800-3_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Boonstoppel","year":"2008","unstructured":"Boonstoppel, P., Cadar, C., Engler, D.: RWset: Attacking Path Explosion in Constraint-Based Test Generation. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 351\u2013366. Springer, Heidelberg (2008)"},{"key":"14_CR9","unstructured":"Cadar, C., Dunbar, D., Engler, D.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of OSDI, pp. 209\u2013224. USENIX Association (2008)"},{"key":"14_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1455518.1455522","volume":"12","author":"C. Cadar","year":"2008","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: Automatically generating inputs of death. ACM Trans. Inf. Syst. Secur.\u00a012, 1\u201338 (2008)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Chelf, B., Hallem, S., Engler, D.: How to write system-specific, static checkers in metal. In: Proceedings of PASTE, pp. 51\u201360. ACM (2002)","DOI":"10.1145\/634636.586097"},{"issue":"5","key":"14_CR12","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1145\/384264.379002","volume":"34","author":"A. Chou","year":"2000","unstructured":"Chou, A., Chelf, B., Engler, D., Heinrich, M.: Using meta-level compilation to check FLASH protocol code. ACM SIGOPS Oper. Syst. Rev.\u00a034(5), 59\u201370 (2000)","journal-title":"ACM SIGOPS Oper. Syst. Rev."},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: Proceedings of PLDI. SIGPLAN, vol.\u00a037(5). ACM Press (2002)","DOI":"10.1145\/543552.512538"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"De Lucia, A.: Program slicing: methods and applications. In: Proceedings of SCAM, pp. 142\u2013149. IEEE Computer Society (2001)","DOI":"10.1109\/SCAM.2001.972675"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Engler, D., Chelf, B., Chou, A., Hallem, S.: Checking system rules using system-specific, programmer-written compiler extensions. In: Proceedings of OSDI, pp. 1\u201316. ACM (2000)","DOI":"10.21236\/ADA419626"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Engler, D., Chen, D., Hallem, S., Chou, A., Chelf, B.: Bugs as deviant behavior: A general approach to inferring errors in systems code. In: Proceedings of SOSP, pp. 57\u201372. ACM (2001)","DOI":"10.1145\/502059.502041"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Compositional dynamic test generation. In: Proceedings of POPL, pp. 47\u201354. ACM (2007)","DOI":"10.1145\/1190215.1190226"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Kiezun, A., Levin, M.Y.: Grammar-based whitebox fuzzing. In: Proceedings of PLDI, pp. 206\u2013215. ACM (2008)","DOI":"10.1145\/1379022.1375607"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of PLDI, pp. 213\u2013223. ACM (2005)","DOI":"10.1145\/1064978.1065036"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: Active property checking. In: Proceedings of EMSOFT, pp. 207\u2013216. ACM (2008)","DOI":"10.1145\/1450058.1450087"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.D.: Compositional must program analysis: unleashing the power of alternation. In: Proceedings of POPL, pp. 43\u201356. ACM (2010)","DOI":"10.1145\/1707801.1706307"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Gupta, R., Harrold, M.J., Soffa, M.L.: An approach to regression testing using slicing. In: Proceedings of ICSM, pp. 299\u2013308. IEEE (1992)","DOI":"10.1109\/ICSM.1992.242531"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"Hallem, S., Chelf, B., Xie, Y., Engler, D.R.: A system and language for building system-specific, static analyses. In: Proceedings of PLDI, pp. 69\u201382. ACM (2002)","DOI":"10.1145\/543552.512539"},{"issue":"7","key":"14_CR25","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J.C. King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Communications of ACM\u00a019(7), 385\u2013394 (1976)","journal-title":"Communications of ACM"},{"key":"14_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-00768-2_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A.V. Nori","year":"2009","unstructured":"Nori, A.V., Rajamani, S.K., Tetali, S., Thakur, A.V.: The Yogi Project: Software Property Checking via Static Analysis and Testing. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 178\u2013181. Springer, Heidelberg (2009)"},{"key":"14_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-25929-6_16","volume-title":"Mathematical and Engineering Methods in Computer Science","author":"J. Obdr\u017e\u00e1lek","year":"2012","unstructured":"Obdr\u017e\u00e1lek, J., Slab\u00fd, J., Trt\u00edk, M.: STANSE: Bug-Finding Framework for C Programs. In: Kot\u00e1sek, Z., Bouda, J., \u010cern\u00e1, I., Sekanina, L., Vojnar, T., Anto\u0161, D. (eds.) MEMICS 2011. LNCS, vol.\u00a07119, pp. 167\u2013178. Springer, Heidelberg (2012)"},{"key":"14_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"669","DOI":"10.1007\/978-3-642-22110-1_55","volume-title":"Computer Aided Verification","author":"D.A. Ramos","year":"2011","unstructured":"Ramos, D.A., Engler, D.R.: Practical, Low-Effort Equivalence Verification of Real Code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 669\u2013685. Springer, Heidelberg (2011)"},{"key":"14_CR29","doi-asserted-by":"crossref","unstructured":"Reps, T., Horowitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Proceedings of POPL, pp. 49\u201361. ACM (1995)","DOI":"10.1145\/199448.199462"},{"key":"14_CR30","doi-asserted-by":"crossref","unstructured":"Saxena, P., Poosankam, P., McCamant, S., Song, D.: Loop-extended symbolic execution on binary programs. In: Proceedings of ISSTA, pp. 225\u2013236. ACM (2009)","DOI":"10.21236\/ADA538843"},{"key":"14_CR31","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Proceedings of ESEC\/FSE, vol.\u00a030, pp. 263\u2013272. ACM (2005)","DOI":"10.1145\/1095430.1081750"},{"key":"14_CR32","first-page":"121","volume":"3","author":"F. Tip","year":"1995","unstructured":"Tip, F.: A survey of program slicing techniques. Journal of Programming Languages\u00a03, 121\u2013189 (1995)","journal-title":"Journal of Programming Languages"},{"issue":"4","key":"14_CR33","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1109\/TSE.1984.5010248","volume":"10","author":"M. Weiser","year":"1984","unstructured":"Weiser, M.: Program slicing. IEEE Transactions on Software Engineering\u00a010(4), 352\u2013357 (1984)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"14_CR34","doi-asserted-by":"crossref","unstructured":"Xu, R.G., Godefroid, P., Majumdar, R.: Testing for buffer overflows with length abstraction. In: Proceedings of ISSTA, pp. 27\u201338. ACM (2008)","DOI":"10.1145\/1390630.1390636"},{"key":"14_CR35","unstructured":"LLVM, http:\/\/llvm.org\/"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32469-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T01:35:51Z","timestamp":1743989751000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-32469-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642324680","9783642324697"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32469-7_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}