{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T20:18:55Z","timestamp":1725740335448},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642397981"},{"type":"electronic","value":"9783642397998"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39799-8_65","type":"book-chapter","created":{"date-parts":[[2013,7,10]],"date-time":"2013-07-10T19:13:06Z","timestamp":1373483586000},"page":"912-927","source":"Crossref","is-referenced-by-count":6,"title":["Programs from Proofs \u2013 A PCC Alternative"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Wonisch","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Schremmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"65_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/3-540-45319-9_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2001","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian Abstraction for Model Checking C Programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 268\u2013283. Springer, Heidelberg (2001)"},{"key":"65_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45139-0_7","volume-title":"Model Checking Software","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 103\u2013122. Springer, Heidelberg (2001)"},{"key":"65_CR3","unstructured":"Bauer, L., Schneider, M.A., Felten, E.W., Appel, A.W.: Access control on the web using proof-carrying authorization. In: Proceedings of the 3rd DARPA Information Survivability Conference and Exposition, DISCEX (2), pp. 117\u2013119 (2003)"},{"key":"65_CR4","unstructured":"Beyer, D., Keremoglu, M., Wendler, P.: Predicate Abstraction with Adjustable-Block Encoding. In: FMCAD 2010, pp. 189\u2013197 (2010)"},{"key":"65_CR5","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.\u00a03148, pp. 2\u201318. Springer, Heidelberg (2004)"},{"key":"65_CR6","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Keremoglu, M.E., Wendler, P.: Conditional model checking: a technique to pass information between verifiers. In: Tracz, W., Robillard, M.P., Bultan, T. (eds.) SIGSOFT FSE, p. 57. ACM (2012)","DOI":"10.1145\/2393596.2393664"},{"key":"65_CR7","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: Ferrante, J., McKinley, K.S. (eds.) PLDI, pp. 300\u2013309. ACM (2007)","DOI":"10.1145\/1273442.1250769"},{"key":"65_CR8","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.\u00a06806, pp. 184\u2013190. Springer, Heidelberg (2011)"},{"key":"65_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-642-16612-9_15","volume-title":"Runtime Verification","author":"E. Bodden","year":"2010","unstructured":"Bodden, E., Lam, P., Hendren, L.: Clara: A Framework for Partially Evaluating Finite-State Runtime Monitors Ahead of Time. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Ro\u015fu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol.\u00a06418, pp. 183\u2013197. Springer, Heidelberg (2010)"},{"key":"65_CR10","doi-asserted-by":"crossref","unstructured":"Crary, K., Weirich, S.: Resource bound certification. In: Proceedings of the ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), pp. 184\u2013198 (2000)","DOI":"10.1145\/325694.325716"},{"key":"65_CR11","doi-asserted-by":"crossref","unstructured":"Das, M., Lerner, S., Seigle, M.: ESP: Path-Sensitive Program Verification in Polynomial Time. In: PLDI, pp. 57\u201368 (2002)","DOI":"10.1145\/543552.512538"},{"key":"65_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/11823230_27","volume-title":"Static Analysis","author":"D. Dhurjati","year":"2006","unstructured":"Dhurjati, D., Das, M., Yang, Y.: Path-sensitive dataflow analysis with iterative refinement. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 425\u2013442. Springer, Heidelberg (2006)"},{"key":"65_CR13","doi-asserted-by":"crossref","unstructured":"Drzevitzky, S., Kastens, U., Platzner, M.: Proof-carrying hardware: Towards runtime verification of reconfigurable modules. In: Proceedings of the International Conference on Reconfigurable Computing (ReConFig), pp. 189\u2013194. IEEE (2009)","DOI":"10.1109\/ReConFig.2009.31"},{"key":"65_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/11691372_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M.B. Dwyer","year":"2006","unstructured":"Dwyer, M.B., Hatcliff, J., Hoosier, M., Ranganath, V.P., Robby, Wallentine, T.: Evaluating the effectiveness of slicing for model reduction of concurrent object-oriented programs. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 73\u201389. Springer, Heidelberg (2006)"},{"key":"65_CR15","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Purandare, R.: Residual dynamic typestate analysis exploiting static analysis: results to reformulate and reduce the cost of dynamic analysis. In: ASE, pp. 124\u2013133. ACM (2007)","DOI":"10.1145\/1321631.1321651"},{"key":"65_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"issue":"2","key":"65_CR17","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1145\/129630.129637","volume":"35","author":"R. Gray","year":"1992","unstructured":"Gray, R., Levi, S., Heuring, V., Sloane, A., Waite, W.: Eli: A complete, flexible compiler construction system. Communications of the ACM\u00a035(2), 121\u2013130 (1992)","journal-title":"Communications of the ACM"},{"key":"65_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/3-540-45657-0_45","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G.C., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 526\u2013538. Springer, Heidelberg (2002)"},{"key":"65_CR19","series-title":"Lecture Notes in Computer Science","first-page":"332","volume-title":"Verification: Theory and Practice","author":"T.A. Henzinger","year":"2004","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.\u00a02772, pp. 332\u2013358. Springer, Heidelberg (2004)"},{"issue":"4","key":"65_CR20","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1002\/spe.438","volume":"32","author":"X. Leroy","year":"2002","unstructured":"Leroy, X.: Bytecode verification on java smart cards. Softw. Pract. Exper.\u00a032(4), 319\u2013340 (2002)","journal-title":"Softw. Pract. Exper."},{"key":"65_CR21","first-page":"106","volume-title":"POPL 1997","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-carrying code. In: POPL 1997, pp. 106\u2013119. ACM, New York (1997)"},{"key":"65_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/3-540-68671-1_5","volume-title":"Mobile Agents and Security","author":"G.C. Necula","year":"1998","unstructured":"Necula, G.C., Lee, P.: Safe, untrusted agents using proof-carrying code. In: Vigna, G. (ed.) Mobile Agents and Security. LNCS, vol.\u00a01419, pp. 61\u201391. Springer, Heidelberg (1998)"},{"key":"65_CR23","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. Journal of Automated Reasoning\u00a031, 303\u2013334 (2003)","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"65_CR24","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1109\/TSE.1986.6312929","volume":"12","author":"R.E. Strom","year":"1986","unstructured":"Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Software Eng.\u00a012(1), 157\u2013171 (1986)","journal-title":"IEEE Trans. Software Eng."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39799-8_65","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T14:43:30Z","timestamp":1557931410000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39799-8_65"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397981","9783642397998"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39799-8_65","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}