{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:52:26Z","timestamp":1740099146196,"version":"3.37.3"},"publisher-location":"Cham","reference-count":50,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319961415"},{"type":"electronic","value":"9783319961422"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96142-2_27","type":"book-chapter","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T15:55:08Z","timestamp":1532102108000},"page":"447-466","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Symbolic Liveness Analysis of Real-World Software"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Schemmel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julian","family":"B\u00fcning","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oscar","family":"Soria Dustmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Noll","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Klaus","family":"Wehrle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"issue":"1","key":"27_CR1","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1145\/59287.62028","volume":"11","author":"B Alpern","year":"1989","unstructured":"Alpern, B., Schneider, F.B.: Verifying temporal properties without temporal logic. ACM Trans. Program. Lang. Syst. 11(1), 147\u2013167 (1989)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"4","key":"27_CR2","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181\u2013185 (1985)","journal-title":"Inf. Process. Lett."},{"issue":"3","key":"27_CR3","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117\u2013126 (1987)","journal-title":"Distrib. Comput."},{"key":"27_CR4","doi-asserted-by":"crossref","unstructured":"Aumasson, J.P., Neves, S., Wilcox-O\u2019Hearn, Z., Winnerlein, C.: BLAKE2: simpler, smaller, fast as MD5. In: Proceedings of the 11th International Conference on Applied Cryptography and Network Security (ACNS 2013), pp. 119\u2013135, June 2013","DOI":"10.1007\/978-3-642-38980-1_8"},{"key":"27_CR5","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"issue":"1","key":"27_CR6","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/s10009-002-0095-0","volume":"5","author":"T Ball","year":"2003","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstraction for model checking C programs. Int. J. Softw. Tools Technol. Transf. 5(1), 49\u201358 (2003)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"27_CR7","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 and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-662-54577-5_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Borralleras","year":"2017","unstructured":"Borralleras, C., Brockschmidt, M., Larraz, D., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Proving termination through conditional termination. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 99\u2013117. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_6"},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"Burnim, J., Jalbert, N., Stergiou, C., Sen, K.: Looper: lightweight detection of infinite loops at runtime. In: Proceedings of the 24th IEEE\/ACM International Conference on Automated Software Engineering (ASE 2009), November 2009","DOI":"10.1109\/ASE.2009.87"},{"key":"27_CR10","unstructured":"Cadar, C., Dunbar, D., Engler, D.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008), December 2008"},{"issue":"2","key":"27_CR11","doi-asserted-by":"crossref","first-page":"10","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. 12(2), 10 (2008)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"issue":"2","key":"27_CR12","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1145\/2408776.2408795","volume":"56","author":"C Cadar","year":"2013","unstructured":"Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun. ACM 56(2), 82\u201390 (2013)","journal-title":"Commun. ACM"},{"issue":"7","key":"27_CR13","doi-asserted-by":"crossref","first-page":"498","DOI":"10.1109\/32.708566","volume":"24","author":"W Chan","year":"1998","unstructured":"Chan, W., Anderson, R.J., Beame, P., Burns, S., Modugno, F., Notkin, D., Reese, J.D.: Model checking large software specifications. IEEE Trans. Softw. Eng. 24(7), 498\u2013520 (1998)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"27_CR14","doi-asserted-by":"crossref","unstructured":"Chen, H.Y., Cook, B., Fuhs, C., Nimkar, K., O\u2019Hearn, P.W.: Proving nontermination via safety. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014), April 2014","DOI":"10.1007\/978-3-642-54862-8_11"},{"key":"27_CR15","doi-asserted-by":"crossref","unstructured":"Chipounov, V., Kuznetsov, V., Candea, G.: S2E: a platform for in vivo multi-path analysis of software systems. In: Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2011), March 2011","DOI":"10.1145\/1950365.1950396"},{"key":"27_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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 Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"issue":"2","key":"27_CR17","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/BF01383968","volume":"6","author":"EM Clarke","year":"1995","unstructured":"Clarke, E.M., Grumberg, O., Hiraishi, H., Jha, S., Long, D.E., McMillan, K.L., Ness, L.A.: Verification of the Futurebus+ cache coherence protocol. Formal Methods Syst. Des. 6(2), 217\u2013232 (1995)","journal-title":"Formal Methods Syst. Des."},{"issue":"4","key":"27_CR18","doi-asserted-by":"crossref","first-page":"957","DOI":"10.1109\/TSE.2011.59","volume":"38","author":"L Cordeiro","year":"2012","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. IEEE Trans. Softw. Eng. 38(4), 957\u2013974 (2012)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"27_CR19","doi-asserted-by":"crossref","unstructured":"Falke, S., Merz, F., Sinz, C.: The bounded model checker LLBMC. In: ASE 2013, pp. 706\u2013709 (2013)","DOI":"10.1109\/ASE.2013.6693138"},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"Ganesh, V., Dill, D.L.: A Decision procedure for bit-vectors and arrays. In: Proceedings of the 19th International Conference on Computer-Aided Verification (CAV 2007), pp. 519\u2013531, July 2007","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"27_CR21","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using VeriSoft. In: POPL 1997, pp. 174\u2013186. ACM (1997)","DOI":"10.1145\/263699.263717"},{"key":"27_CR22","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of the Conference on Programming Language Design and Implementation (PLDI 2005), vol. 40, pp. 213\u2013223, June 2005","DOI":"10.1145\/1065010.1065036"},{"issue":"1","key":"27_CR23","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1145\/2090147.2094081","volume":"10","author":"P Godefroid","year":"2012","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.: SAGE: whitebox fuzzing for security testing. ACM Queue 10(1), 20 (2012)","journal-title":"ACM Queue"},{"key":"27_CR24","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. In: Proceedings of the 15th Network and Distributed System Security Symposium (NDSS 2008), vol. 8, pp. 151\u2013166, February 2008"},{"key":"27_CR25","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: Proceedings of the Conference on Programming Language Design and Implementation (PLDI 2008), June 2008","DOI":"10.1145\/1375581.1375616"},{"key":"27_CR26","doi-asserted-by":"crossref","unstructured":"Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.G.: Proving non-termination. In: POPL 2008, pp. 147\u2013158. ACM (2008)","DOI":"10.1145\/1328438.1328459"},{"issue":"4","key":"27_CR27","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. Int. J. Softw. Tools Technol. Transf. 2(4), 366\u2013381 (2000)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"27_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/978-3-319-41591-8_16","volume-title":"Software Engineering and Formal Methods","author":"J Hensel","year":"2016","unstructured":"Hensel, J., Giesl, J., Frohn, F., Str\u00f6der, T.: Proving termination of programs with bitvector arithmetic by symbolic execution. In: De Nicola, R., K\u00fchn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 234\u2013252. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41591-8_16"},{"issue":"4","key":"27_CR29","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/s100090050039","volume":"2","author":"G Holzmann","year":"2000","unstructured":"Holzmann, G., Najm, E., Serhrouchni, A.: Spin model checking: an introduction. Int. J. Softw. Tools Technol. Transf. 2(4), 321\u2013327 (2000)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"9","key":"27_CR30","doi-asserted-by":"crossref","first-page":"981","DOI":"10.1016\/0169-7552(93)90095-L","volume":"25","author":"GJ Holzmann","year":"1993","unstructured":"Holzmann, G.J.: Design and validation of protocols: a tutorial. Comput. Netw. ISDN Syst. 25(9), 981\u20131017 (1993)","journal-title":"Comput. Netw. ISDN Syst."},{"key":"27_CR31","first-page":"268","volume":"53","author":"E Kindler","year":"1994","unstructured":"Kindler, E.: Safety and liveness properties: a survey. Bull. Eur. Assoc. Theor. Comput. Sci. 53, 268\u2013272 (1994)","journal-title":"Bull. Eur. Assoc. Theor. Comput. Sci."},{"key":"27_CR32","doi-asserted-by":"crossref","unstructured":"Kling, M., Misailovic, S., Carbin, M., Rinard, M.: Bolt: on-demand infinite loop escape in unmodified binaries. In: Proceedings of the 27th Annual Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2012), October 2012","DOI":"10.1145\/2384616.2384648"},{"key":"27_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1007\/978-3-642-22110-1_44","volume-title":"Computer Aided Verification","author":"D Kroening","year":"2011","unstructured":"Kroening, D., Ouaknine, J., Strichman, O., Wahl, T., Worrell, J.: Linear completeness thresholds for bounded model checking. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 557\u2013572. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_44"},{"issue":"3","key":"27_CR34","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291\u2013314 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"27_CR35","doi-asserted-by":"crossref","unstructured":"Larraz, D., Nimkar, K., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Proving non-termination using Max-SMT. In: Proceedings of the 26th International Conference on Computer-Aided Verification (CAV 2014), July 2014","DOI":"10.1007\/978-3-319-08867-9_52"},{"key":"27_CR36","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: Proceedings of the 2nd International Symposium on Code Generation and Optimization (CGO 2004), San Jose, CA, USA, pp. 75\u201388, March 2004","DOI":"10.1109\/CGO.2004.1281665"},{"key":"27_CR37","doi-asserted-by":"crossref","unstructured":"Liew, D., Schemmel, D., Cadar, C., Donaldson, A.F., Z\u00e4hl, R., Wehrle, K.: Floating-point symbolic execution: a case study in N-version programming. In: Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE 2017), pp. 601\u2013612, October\u2013November 2017","DOI":"10.1109\/ASE.2017.8115670"},{"key":"27_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-27705-4_12","volume-title":"Verified Software: Theories, Tools, Experiments","author":"F Merz","year":"2012","unstructured":"Merz, F., Falke, S., Sinz, C.: LLBMC: bounded model checking of C and C++ programs using a compiler IR. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 146\u2013161. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27705-4_12"},{"key":"27_CR39","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), pp. 337\u2013340, March\u2013April 2008","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"3","key":"27_CR40","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S Owicki","year":"1982","unstructured":"Owicki, S., Lamport, L.: Proving liveness properties of concurrent programs. TOPLAS 4(3), 455\u2013495 (1982)","journal-title":"TOPLAS"},{"key":"27_CR41","doi-asserted-by":"crossref","unstructured":"Sasnauskas, R., Landsiedel, O., Alizai, M.H., Weise, C., Kowalewski, S., Wehrle, K.: KleeNet: discovering insidious interaction bugs in wireless sensor networks before deployment. In: Proceedings of the 9th ACM\/IEEE International Conference on Information Processing in Sensor Networks (IPSN 2010), April 2010","DOI":"10.1145\/1791212.1791235"},{"key":"27_CR42","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Proceedings of the Conference on Programming Language Design and Implementation (PLDI 2005), vol. 30, pp. 263\u2013272, June 2005","DOI":"10.1145\/1081706.1081750"},{"issue":"5","key":"27_CR43","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1109\/2.841786","volume":"33","author":"J Straunstrup","year":"2000","unstructured":"Straunstrup, J., Andersen, H.R., Hulgaard, H., Lind-Nielsen, J., Behrmann, G., Kristoffersen, K., Skou, A., Leerberg, H., Theilgaard, N.B.: Practical verification of embedded software. Computer 33(5), 68\u201375 (2000)","journal-title":"Computer"},{"key":"27_CR44","unstructured":"The BusyBox Developers: BusyBox: The Swiss Army Knife of Embedded Linux, August 2017, version 1.27.2. https:\/\/busybox.net"},{"key":"27_CR45","unstructured":"The GNU Project: GNU Coreutils, January 2016, version 8.25. https:\/\/www.gnu.org\/software\/coreutils"},{"key":"27_CR46","unstructured":"The GNU Project: GNU sed, February 2017, version 4.4. https:\/\/www.gnu.org\/software\/sed"},{"key":"27_CR47","unstructured":"The KLEE Team: OSDI 2008 Coreutils Experiments. http:\/\/klee.github.io\/docs\/coreutils-experiments\/ . Section 07"},{"key":"27_CR48","unstructured":"The toybox Developers: toybox, October 2017, version 0.7.5. http:\/\/landley.net\/toybox"},{"key":"27_CR49","doi-asserted-by":"crossref","unstructured":"Tillmann, N., De Halleux, J.: Pex-white box test generation for .NET. In: Proceedings of the 2nd International Conference on Tests and Proofs (TAP 2008), pp. 134\u2013153, April 2008","DOI":"10.1007\/978-3-540-79124-9_10"},{"issue":"2","key":"27_CR50","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1023\/A:1011236117591","volume":"19","author":"J Tretmans","year":"2001","unstructured":"Tretmans, J., Wijbrans, K., Chaudron, M.: Software engineering with formal methods: the development of a storm surge barrier control system revisiting seven myths of formal methods. Formal Methods Syst. Des. 19(2), 195\u2013215 (2001)","journal-title":"Formal Methods Syst. Des."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96142-2_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T23:21:05Z","timestamp":1571613665000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96142-2_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319961415","9783319961422"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96142-2_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}