{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T10:49:15Z","timestamp":1761562155773,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319471655"},{"type":"electronic","value":"9783319471662"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47166-2_53","type":"book-chapter","created":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T18:07:34Z","timestamp":1475604454000},"page":"749-765","source":"Crossref","is-referenced-by-count":8,"title":["Deductive Verification of Legacy Code"],"prefix":"10.1007","author":[{"given":"Bernhard","family":"Beckert","sequence":"first","affiliation":[]},{"given":"Thorsten","family":"Bormer","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Grahl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,5]]},"reference":[{"key":"53_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/978-3-319-12154-3_4","volume-title":"Verified Software: Theories, Tools and Experiments","author":"W Ahrendt","year":"2014","unstructured":"Ahrendt, W., et al.: The KeY platform for verification and analysis of Java programs. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 55\u201371. Springer, Heidelberg (2014)"},{"key":"53_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1007\/978-3-642-15057-9_3","volume-title":"Verified Software: Theories, Tools, Experiments","author":"E Alkassar","year":"2010","unstructured":"Alkassar, E., Hillebrand, M.A., Paul, W., Petrova, E.: Automated verification of a small hypervisor. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 40\u201354. Springer, Heidelberg (2010)"},{"key":"53_CR3","doi-asserted-by":"crossref","unstructured":"Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Lessons learned from microkernel verification: specification is the new bottleneck. In: Cassez, F., Huuck, R., Klein, G., Schlich, B. (eds.) 7th Conference on Systems Software Verification. SSV 2012, Sydney, Australia, vol. 102. Electronic Proceedings in Theoretical Computer Science (2012)","DOI":"10.4204\/EPTCS.102.4"},{"key":"53_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1007\/978-3-642-31762-0_7","volume-title":"Formal Verification of Object-Oriented Software","author":"B Beckert","year":"2012","unstructured":"Beckert, B., Bormer, T., Merz, F., Sinz, C.: Integration of bounded model checking and deductive verification. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol. 7421, pp. 86\u2013104. Springer, Heidelberg (2012)"},{"key":"53_CR5","doi-asserted-by":"crossref","unstructured":"Bhattacharya, P., Iliofotou, M., Neamtiu, I., Faloutsos, M.: Graph-based analysis and prediction for software evolution. In: Glinz, M., Murphy, G.C., Pezz\u00e8, M. (eds.) 34th International Conference on Software Engineering (ICSE 2012), pp. 419\u2013429. IEEE (2012)","DOI":"10.1109\/ICSE.2012.6227173"},{"key":"53_CR6","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, Wroclaw, Poland, pp. 53\u201364 (2011)"},{"issue":"6","key":"53_CR7","doi-asserted-by":"crossref","first-page":"729","DOI":"10.1007\/s10009-013-0293-y","volume":"17","author":"D Bruns","year":"2015","unstructured":"Bruns, D., Mostowski, W., Ulbrich, M.: Implementation-level verification of algorithms with KeY. Softw. Tools Technol. Transf. 17(6), 729\u2013744 (2015)","journal-title":"Softw. Tools Technol. Transf."},{"key":"53_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1007\/978-3-662-45231-8_9","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"R Bubel","year":"2014","unstructured":"Bubel, R., H\u00e4hnle, R., Pelevina, M.: Fully abstract operation contracts. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part II. LNCS, vol. 8803, pp. 120\u2013134. Springer, Heidelberg (2014)"},{"key":"53_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"issue":"4","key":"53_CR10","doi-asserted-by":"crossref","first-page":"761","DOI":"10.1007\/s00165-013-0278-3","volume":"26","author":"F Damiani","year":"2014","unstructured":"Damiani, F., Dovland, J., Johnsen, E.B., Schaefer, I.: Verifying traits: an incremental proof system for fine-grained reuse. Formal Asp. Comput. 26(4), 761\u2013793 (2014)","journal-title":"Formal Asp. Comput."},{"key":"53_CR11","doi-asserted-by":"crossref","unstructured":"Delahaye, M., Kosmatov, N., Signoles, J.: Common specification language for static and dynamic analysis of C programs. In: Shin, S.Y., Maldonado, J.C. (eds.) Proceedings of the 28th Annual ACM Symposium on Applied Computing, SAC 2013, Coimbra, Portugal, 18\u201322 March 2013, pp. 1230\u20131235. ACM (2013)","DOI":"10.1145\/2480362.2480593"},{"issue":"7","key":"53_CR12","doi-asserted-by":"crossref","first-page":"578","DOI":"10.1016\/j.jlap.2010.07.008","volume":"79","author":"J Dovland","year":"2010","unstructured":"Dovland, J., Johnsen, E.B., Owe, O., Steffen, M.: Lazy behavioral subtyping. J. Logic Algebraic Program. 79(7), 578\u2013607 (2010)","journal-title":"J. Logic Algebraic Program."},{"key":"53_CR13","doi-asserted-by":"crossref","unstructured":"Falke, S., Merz, F., Sinz, C.: The bounded model checker LLBMC. In: Denney, E., Bultan, T., Zeller, A. (eds.) 28th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2013, Silicon Valley, CA, USA. IEEE (2013)","DOI":"10.1109\/ASE.2013.6693138"},{"key":"53_CR14","doi-asserted-by":"crossref","unstructured":"Felsing, D., Grebing, S., Klebanov, V., R\u00fcmmer, P., Ulbrich, M.: Automating regression verification. In: 29th IEEE\/ACM International Conference on Automated Software Engineering (ASE 2014), pp. 349\u2013360. ACM (2014)","DOI":"10.1145\/2642937.2642987"},{"key":"53_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/978-3-642-24690-6_28","volume-title":"Software Engineering and Formal Methods","author":"C Goues Le","year":"2011","unstructured":"Le Goues, C., Leino, K.R.M., Moskal, M.: The Boogie verification debugger (Tool Paper). In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 407\u2013414. Springer, Heidelberg (2011)"},{"key":"53_CR16","unstructured":"Grahl, D.: Deductive verification of concurrent programs and its application to secure information flow for Java. Ph.D. thesis, Karlsruhe Inst. of Techn. (2015)"},{"issue":"6","key":"53_CR17","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/s10207-009-0086-1","volume":"8","author":"C Hammer","year":"2009","unstructured":"Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. Int. J. Inf. Secur. 8(6), 399\u2013422 (2009)","journal-title":"Int. J. Inf. Secur."},{"key":"53_CR18","unstructured":"Hawblitzel, C., Howell, J., Lorch, J.R., Narayan, A., Parno, B., Zhang, D., Zill, B.: Ironclad apps: end-to-end security via automated full-system verification. In: Flinn, J., Levy, H. (eds.) 11th USENIX Symposium on Operating Systems Design and Implementation, pp. 165\u2013181. USENIX Association (2014)"},{"key":"53_CR19","unstructured":"Hentschel, M.: Integrating symbolic execution, debugging and verification. Ph.D. thesis, Technische Universit\u00e4t Darmstadt, January 2016"},{"key":"53_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/978-3-319-10181-1_4","volume-title":"Integrated Formal Methods","author":"M Hentschel","year":"2014","unstructured":"Hentschel, M., K\u00e4sdorf, S., H\u00e4hnle, R., Bubel, R.: An interactive verification tool meets an IDE. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 55\u201370. Springer, Heidelberg (2014)"},{"key":"53_CR21","unstructured":"Herda, M.: Generating bounded counterexamples for KeY proof obligations. Master\u2019s thesis, KIT (2014). http:\/\/dx.doi.org\/10.5445\/IR\/1000055929"},{"key":"53_CR22","unstructured":"Kaiser, R., Wagner, S.: Evolution of the PikeOS microkernel. In: Kuz, I., Petters, S.M. (eds.) 1st International Workshop on Microkernels for Embedded Systems (MIKES 2007). National ICT Australia (2007)"},{"issue":"6","key":"53_CR23","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G Klein","year":"2010","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an operating-system kernel. Commun. ACM 53(6), 107\u2013115 (2010). doi: 10.1145\/1743546.1743574","journal-title":"Commun. ACM"},{"issue":"1","key":"53_CR24","doi-asserted-by":"crossref","first-page":"2: 1","DOI":"10.1145\/2560537","volume":"32","author":"G Klein","year":"2014","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Murray, T., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1), 2: 1\u20132: 70 (2014)","journal-title":"ACM Trans. Comput. Syst."},{"key":"53_CR25","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Truderung, T., Beckert, B., Bruns, D., Kirsten, M., Mohr, M.: A hybrid approach for proving noninterference of Java programs. In: Fournet, C., Hicks, M., Vigan\u00f2, L. (eds.) 28th IEEE Computer Security Foundations Symposium (CSF) (2015)","DOI":"10.1109\/CSF.2015.28"},{"key":"53_CR26","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Truderung, T., Vogt, A.: Verifiability, privacy, and coercion-resistance: new insights from a case study. In: Proceedings of the 32nd IEEE Symposium on Security and Privacy (S&P), pp. 538\u2013553. IEEE Computer Society (2011)","DOI":"10.1109\/SP.2011.21"},{"key":"53_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"key":"53_CR28","unstructured":"Leino, K.R.M., Moskal, M.: Usable auto-active verification. In: Usable Verification Workshop (2010). http:\/\/fm.csl.sri.com\/UV10"},{"key":"53_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/978-3-642-21437-0_8","volume-title":"FM 2011: Formal Methods","author":"P M\u00fcller","year":"2011","unstructured":"M\u00fcller, P., Ruskiewicz, J.N.: Using debuggers to understand failed verification attempts. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 73\u201387. Springer, Heidelberg (2011)"},{"key":"53_CR30","series-title":"LNCS","volume-title":"Isabelle\u2013A Generic Theorem Prover","author":"LC Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle\u2013A Generic Theorem Prover. LNCS, vol. 828. Springer, Heidelberg (1994)"},{"key":"53_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/978-3-642-40787-1_15","volume-title":"Runtime Verification","author":"N Polikarpova","year":"2013","unstructured":"Polikarpova, N., Furia, C.A., West, S.: To run what no one has run before: executing an intermediate verification language. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 251\u2013268. Springer, Heidelberg (2013)"},{"key":"53_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28\u201332. Springer, Heidelberg (2008)"},{"key":"53_CR33","unstructured":"Wenzel, M.M.: Isabelle\/Isar\u2013a versatile environment for human-readable formal proof documents. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2002)"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47166-2_53","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T20:22:08Z","timestamp":1498335728000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47166-2_53"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319471655","9783319471662"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47166-2_53","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}