{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T08:37:55Z","timestamp":1743064675753,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661964"},{"type":"electronic","value":"9783319661971"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66197-1_8","type":"book-chapter","created":{"date-parts":[[2017,8,11]],"date-time":"2017-08-11T21:02:30Z","timestamp":1502485350000},"page":"120-135","source":"Crossref","is-referenced-by-count":3,"title":["PART$$_\\mathrm {PW}$$: From Partial Analysis Results to a Proof Witness"],"prefix":"10.1007","author":[{"given":"Marie-Christine","family":"Jakobs","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,13]]},"reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-27864-1_2","volume-title":"Static Analysis","author":"D Beyer","year":"2004","unstructured":"Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: The Blast query language for software verification. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 2\u201318. Springer, Heidelberg (2004). doi:\n10.1007\/978-3-540-27864-1_2"},{"key":"8_CR2","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Keremoglu, M.E., Wendler, P.: Conditional model checking: A technique to pass information between verifiers. In: FSE, pp. 57:1\u201357:11. ACM (2012). doi:\n10.1145\/2393596.2393664","DOI":"10.1145\/2393596.2393664"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-540-73368-3_51","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Configurable software verification: concretizing the convergence of model checking and program analysis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 504\u2013518. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-73368-3_51"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). doi:\n10.1007\/978-3-642-22110-1_16"},{"key":"8_CR5","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: FMCAD, pp. 189\u2013198. FMCAD Inc. (2010)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-37057-1_11","volume-title":"Fundamental Approaches to Software Engineering","author":"D Beyer","year":"2013","unstructured":"Beyer, D., L\u00f6we, S.: Explicit-state software model checking based on CEGAR and interpolation. In: Cortellessa, V., Varr\u00f3, D. (eds.) FASE 2013. LNCS, vol. 7793, pp. 146\u2013162. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-37057-1_11"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-319-23404-5_12","volume-title":"Model Checking Software","author":"D Beyer","year":"2015","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Benchmarking and resource measurement. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 160\u2013178. Springer, Cham (2015). doi:\n10.1007\/978-3-319-23404-5_12"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11921240_20","volume-title":"Theoretical Aspects of Computing - ICTAC 2006","author":"A Chaieb","year":"2006","unstructured":"Chaieb, A.: Proof-producing program analysis. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 287\u2013301. Springer, Heidelberg (2006). doi:\n10.1007\/11921240_20"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252. ACM (1977). doi:\n10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Dong, Y., Wang, S., Zhang, L., Yang, P.: Modular certification of low-level intermediate representation programs. In: COMPSAC, pp. 563\u2013570. IEEE (2009). doi:\n10.1109\/COMPSAC.2009.81","DOI":"10.1109\/COMPSAC.2009.81"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Feng, X., Ni, Z., Shao, Z., Guo, Y.: An open framework for foundational proof-carrying code. In: TLDI, pp. 67\u201378. ACM (2007). doi:\n10.1145\/1190315.1190325","DOI":"10.1145\/1190315.1190325"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-45139-0_14","volume-title":"Model Checking Software","author":"H Garavel","year":"2001","unstructured":"Garavel, H., Mateescu, R., Smarandache, I.: Parallel state space construction for model-checking. In: Dwyer, M. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 217\u2013234. Springer, Heidelberg (2001). doi:\n10.1007\/3-540-45139-0_14"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-540-30142-4_10","volume-title":"Theorem Proving in Higher Order Logics","author":"NA Hamid","year":"2004","unstructured":"Hamid, N.A., Shao, Z.: Interfacing hoare logic and type systems for foundational proof-carrying code. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 118\u2013135. Springer, Heidelberg (2004). doi:\n10.1007\/978-3-540-30142-4_10"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-540-39910-0_16","volume-title":"Verification: Theory and Practice","author":"TA Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sanvido, M.A.A.: Extreme model checking. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 332\u2013358. Springer, Heidelberg (2003). doi:\n10.1007\/978-3-540-39910-0_16"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-319-22969-0_12","volume-title":"Software Engineering and Formal Methods","author":"M-C Jakobs","year":"2015","unstructured":"Jakobs, M.-C.: Speed up configurable certificate validation by certificate reduction and partitioning. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 159\u2013174. Springer, Cham (2015). doi:\n10.1007\/978-3-319-22969-0_12"},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"Jakobs, M.C., Wehrheim, H.: Certification for configurable program analysis. In: SPIN, pp. 30\u201339. ACM (2014). doi:\n10.1145\/2632362.2632372","DOI":"10.1145\/2632362.2632372"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: A library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661\u2013667. Springer, Heidelberg (2009). doi:\n10.1007\/978-3-642-02658-4_52"},{"issue":"4","key":"8_CR18","doi-asserted-by":"publisher","first-page":"21:1","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R Jhala","year":"2009","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 21:1\u201321:54 (2009). doi:\n10.1145\/1592434.1592438","journal-title":"ACM Comput. Surv."},{"key":"8_CR19","doi-asserted-by":"publisher","unstructured":"Necula, G.C.: Proof-carrying code. In: POPL, pp. 106\u2013119. ACM (1997). doi:\n10.1145\/263699.263712","DOI":"10.1145\/263699.263712"},{"key":"8_CR20","volume-title":"Principles of Program Analysis","author":"F Nielson","year":"2005","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, 1st edn. Springer, Heidelberg (2005). Corr. 2. print. edn","edition":"1"},{"issue":"3","key":"8_CR21","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1023\/B:JARS.0000021015.15794.82","volume":"31","author":"E Rose","year":"2003","unstructured":"Rose, E.: Lightweight bytecode verification. J. Autom. Reasoning 31(3), 303\u2013334 (2003). doi:\n10.1023\/B:JARS.0000021015.15794.82","journal-title":"J. Autom. Reasoning"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-540-40018-9_16","volume-title":"Programming Languages and Systems","author":"S Seo","year":"2003","unstructured":"Seo, S., Yang, H., Yi, K.: Automatic construction of hoare proofs from abstract interpretation results. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol. 2895, pp. 230\u2013245. Springer, Heidelberg (2003). doi:\n10.1007\/978-3-540-40018-9_16"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66197-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,7,24]],"date-time":"2018-07-24T23:48:42Z","timestamp":1532476122000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66197-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661964","9783319661971"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66197-1_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}