{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:29:19Z","timestamp":1725564559798},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540208037"},{"type":"electronic","value":"9783540246220"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24622-0_15","type":"book-chapter","created":{"date-parts":[[2010,9,5]],"date-time":"2010-09-05T11:33:53Z","timestamp":1283686433000},"page":"161-174","source":"Crossref","is-referenced-by-count":2,"title":["Certifying Temporal Properties for Compiled C Programs"],"prefix":"10.1007","author":[{"given":"Songtao","family":"Xia","sequence":"first","affiliation":[]},{"given":"James","family":"Hook","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"Appel, A.: Fundational Proof-carrying Code. In: Proceeding of 16th IEEE Symposium on Logics in Computer Science (June 2001)"},{"key":"15_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.: Automatically ValidatingTemporal Safety Properties of Interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 103\u2013122. Springer, Heidelberg (2001)"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1998","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems compositionally and automatically. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 319\u2013331. Springer, Heidelberg (1998)"},{"key":"15_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/3-540-45620-1_3","volume-title":"Automated Deduction - CADE-18","author":"A. Bernard","year":"2002","unstructured":"Bernard, A., Lee, P.: Temporal Logic for Proof-carrying Code. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 31\u201346. Springer, Heidelberg (2002)"},{"key":"15_CR5","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.M. Clarke","year":"2000","unstructured":"Clarke, E.M., 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":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","volume-title":"Computer Aided Verification","author":"S. Das","year":"1999","unstructured":"Das, S., Dill, D., Park, S.J.: Experience with Predicate Abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 160\u2013171. Springer, Heidelberg (1999)"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"15_CR8","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. Henzinger","year":"2002","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Necula, G., 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":"15_CR9","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: ACM SIGPLANSIGACT Conference on Principles of Programming Languages, pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-44585-4_2","volume-title":"Computer Aided Verification","author":"K.S. Namjoshi","year":"2001","unstructured":"Namjoshi, K.S.: Certifying Model Checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 2. Springer, Heidelberg (2001)"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/3-540-36384-X_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K.S. Namjoshi","year":"2002","unstructured":"Namjoshi, K.S.: Lifting Temporal Proofs through Abstractions. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 174\u2013188. Springer, Heidelberg (2002)"},{"key":"15_CR13","unstructured":"Kozen, D.: Efficient Code Certification, Technical Report, Computer Science Department, Cornell University (1998)"},{"key":"15_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg (1992)"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"McPeak, S., Necula, G.C., Rahul, S.P., Weimer, W.: Cil: Intermediate languages and tools for c program analysis and transformation. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol.\u00a02304, Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45937-5_16"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/BFb0055511","volume-title":"Types in Compilation","author":"G. Morrisett","year":"1998","unstructured":"Morrisett, G., Crary, K., Glew, N., Walker, D.: Stacked-based Typed Assembly Language. In: Leroy, X., Ohori, A. (eds.) TIC 1998. LNCS, vol.\u00a01473, pp. 28\u201352. Springer, Heidelberg (1998)"},{"issue":"3","key":"15_CR17","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1145\/319301.319345","volume":"21","author":"G. Morrisett","year":"1999","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F toTyped Assembly Language. ACM Transactions on Programming Languages and Systems\u00a021(3), 527\u2013568 (1999)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"15_CR18","unstructured":"Necula, G.: Compiling with Proofs. PhD thesis, Carnegie Mellon University (1998)"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Necula, G.: A Scalable Architecture for Proof-Carrying Code (2001)","DOI":"10.1007\/3-540-44716-4_2"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1007\/3-540-58179-0_57","volume-title":"Computer Aided Verification","author":"R. Kurshan","year":"1994","unstructured":"Kurshan, R.: Models Whose Checks Don\u2019t Explode. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 222\u2013233. Springer, Heidelberg (1994)"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Saidi, H.: Model-checking Guided Abstraction and Analysis. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, pp. 377\u2013389. Springer, Heidelberg (2000)","DOI":"10.1007\/978-3-540-45099-3_20"},{"key":"15_CR22","unstructured":"Schwoon, S.: Moped software, available at http:\/\/wwwbrauer.informatik.tu-muenchen.de\/~schwoon\/moped\/"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"Sekar, R., Ramakrishnan, C., Ramakrishnan, I., Smolka, S.: Model-carrying Code (MCC): A New Paradigm for Mobile Code Security. In: New Security Paradigm Workshop (2001)","DOI":"10.1145\/508172.508175"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Sekar, R., Venkatakrishnan, V., Basu, S., Bhatkar, S., DuVarney, D.: Model-carrying code: A practical approach for safe execution of untrusted applications. In: Proceedings of ACM Symposium on Operating System Principles, pp. 15\u201328 (2003)","DOI":"10.1145\/945445.945448"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Shao, Z., Saha, B., Trifonov, V., Papaspyrou, N.: Type System for Certified Binaries. In: Proc. 29th ACM Symposium on Principles of Programming Languages (POPL 2002), January 2002, pp. 217\u2013232 (2002)","DOI":"10.1145\/503272.503293"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Tan, L., Cleaveland, R.: Evidence-based model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 455\u2013470. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-45657-0_37"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Xi, H., Harper, R.: Dependently Typed Assembly Language. In: Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming, September 2001, pp. 169\u2013180 (2001)","DOI":"10.1145\/507635.507657"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Xia, S., Hook, J.: Experience with abstraction-carrying code. In: Proceedigns of Software Model Checking Workshop (2003)","DOI":"10.1016\/S1571-0661(05)80005-2"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Xia, S., Hook, J.: An implementation of abstraction-carrying code. In: Proceedings of Foundations of Computer Security Workshop (2003)","DOI":"10.1016\/S1571-0661(05)80005-2"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24622-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,3]],"date-time":"2019-06-03T17:40:23Z","timestamp":1559583623000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24622-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208037","9783540246220"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24622-0_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}