{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T14:42:32Z","timestamp":1648996952772},"reference-count":25,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3619,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,9]]},"DOI":"10.1016\/s1571-0661(05)80005-2","type":"journal-article","created":{"date-parts":[[2005,5,20]],"date-time":"2005-05-20T09:21:17Z","timestamp":1116580877000},"page":"433-449","source":"Crossref","is-referenced-by-count":2,"title":["Experience with Abstraction-carrying Code"],"prefix":"10.1016","volume":"89","author":[{"given":"Songtao","family":"Xia","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James","family":"Hook","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(05)80005-2_BIB1","series-title":"Proceeding of 16th IEEE Symposium on Logics in Computer Science","article-title":"Fundational Proof-carrying Code","author":"Appel","year":"2001"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB2","series-title":"SPIN2001, Lecture Notes in Computer Science, LNCS2057","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/3-540-45139-0_7","article-title":"Automatically Validating Temporal Safety Properties of Interfaces","author":"Ball","year":"2001"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB3","series-title":"Proceedings of CAV'98, LNCS 1427","first-page":"319","article-title":"Computing abstractions of infinite state systems compositionally and automatically","author":"Bensalem","year":"1998"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB4","series-title":"Proceedings of the 18th International Conference on Automated Deduction (CADE-18), volume 2392 of Lecture Notes in Artificial Intelligence","first-page":"31","article-title":"Temporal Logic for Proof-carrying Code","author":"Bernard","year":"2002"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB5","series-title":"Computer Aided Verification","first-page":"154","article-title":"Counterexample-Guided Abstraction Refinement","author":"Clarke","year":"2000"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB6","series-title":"4th POPL, Los Angeles, CA","first-page":"238","article-title":"Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints","author":"Cousot","year":"1977"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB7","series-title":"Proceedings of CAV'99, LNCS 1633","first-page":"160","article-title":"Experience with Predicate Abstraction","author":"Das","year":"1999"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB8","series-title":"Proceedings of CAV'97, Lecture Notes in Computer Science, LNCS 1254","first-page":"72","article-title":"Construction of Abstract State Graphs with PVS","author":"Graf","year":"1997"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB9","series-title":"Computer-Aided Verification","first-page":"526","article-title":"\u201cTemporal-Safety Proofs for Systems Code","author":"Henzinger","year":"2002"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB10","series-title":"ACM SIGPLAN-SIGACT Conference on Principles of Programming Languages","first-page":"58","article-title":"Lazy abstraction","author":"Henzinger","year":"2002"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB11","series-title":"13th Conference on Computer Aided Verification (CAV)","article-title":"Certifying Model Checkers","author":"Kedar","year":"2001"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB12","series-title":"Lifting Temporal Proofs through Abstractions","author":"Namjoshi","year":"2003"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB13","series-title":"Efficient Code Certification, Technical Report, Computer Science Department","author":"Kozen","year":"1998"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB14","series-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Manna","year":"1992"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB15","series-title":"Proceedings of Conference on Compiler Construction (CC'02)","article-title":"Cil: Intermediate languages and tools for c program analysis and transformation","author":"McPeak","year":"2002"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB16","series-title":"Proceedings of workshop on Types in Compilation, also in Lecture Notes in Computer Science, LNCS 1473","first-page":"28","article-title":"Stacked-based Typed Assembly Language","author":"Morrisett","year":"1998"},{"issue":"3","key":"10.1016\/S1571-0661(05)80005-2_BIB17","doi-asserted-by":"crossref","first-page":"527","DOI":"10.1145\/319301.319345","article-title":"From System F to Typed Assembly Language","volume":"21","author":"Morrisett","year":"1999","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB18","series-title":"Compiling with Proofs, PhD thesis","author":"Necula","year":"1998"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB19","series-title":"A Scalable Architecture for Proof-Carrying Code","author":"Necula","year":"2001"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB20","first-page":"222","article-title":"Models Whose Checks Don't Explode","author":"Kurshan","year":"1994","journal-title":"Computer-Aided Verification"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB21","series-title":"Proceedings of SAS'00, Lecture Notes in Computer Science, LNCS 1824","first-page":"377","article-title":"Model-checking Guided Abstraction and Analysis","author":"Saidi","year":"2000"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB22","series-title":"Proc. 29th ACM Symposium on Principles of Programming Languages (POPL'02)","first-page":"217","article-title":"Type System for Certified Binaries","author":"Shao","year":"2002"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB23","series-title":"13th Conference on Computer Aided Verfication (CAV)","first-page":"455","article-title":"Evidence-based model checking","author":"Tan","year":"2001"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB24","series-title":"Proceedings of Formal Techniques for Java-like Programs","article-title":"Abstract interpretation as certificate for temporal properties","author":"Xia","year":"2003"},{"key":"10.1016\/S1571-0661(05)80005-2_BIB25","series-title":"Proceedings of Foundations of Computer Security Workshop","article-title":"An implementation of abstraction-carrying code","author":"Xia","year":"2003"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105800052?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105800052?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,1,26]],"date-time":"2019-01-26T05:50:27Z","timestamp":1548481827000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105800052"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":25,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["S1571066105800052"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)80005-2","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}