{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T14:26:01Z","timestamp":1730298361102,"version":"3.28.0"},"reference-count":27,"publisher":"IEEE","license":[{"start":{"date-parts":[[2024,5,23]],"date-time":"2024-05-23T00:00:00Z","timestamp":1716422400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2024,5,23]],"date-time":"2024-05-23T00:00:00Z","timestamp":1716422400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/100009224","name":"Advanced Research Projects Agency","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100009224","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024,5,23]]},"DOI":"10.1109\/spw63631.2024.00022","type":"proceedings-article","created":{"date-parts":[[2024,7,4]],"date-time":"2024-07-04T17:29:29Z","timestamp":1720114169000},"page":"180-191","source":"Crossref","is-referenced-by-count":0,"title":["Robust Verification of PEG Parser Interpreters"],"prefix":"10.1109","author":[{"given":"Natarajan","family":"Shankar","sequence":"first","affiliation":[{"name":"SRI International,Menlo Park,CA,94025"}]},{"given":"Zephyr","family":"Lucas","sequence":"additional","affiliation":[{"name":"Dartmouth College,Hanover,NH,03755"}]}],"member":"263","reference":[{"issue":"2","key":"ref1","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/32.345827","article-title":"Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS","volume":"21","author":"Owre","year":"1995","journal-title":"IEEE Transactions on Software Engineering"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964011"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/362007.362035"},{"key":"ref4","first-page":"35","article-title":"Algorithm schemata and data structures in syntactic processing","author":"Kay","year":"1986","journal-title":"Readings in natural language processing"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.3115\/981311.981338"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2020.01.001"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/SWAT.1970.18"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581483"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373836"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/3122975.3122979"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_25"},{"key":"ref12","first-page":"1465","article-title":"Everparse: Verified secure zero-copy parsers for authenticated message formats","volume-title":"28th USENIX Security Symposium, USENIX Security 2019, Santa Clara, CA, USA, August 14-16, 2019","author":"Ramananandro"},{"issue":"ICFP","key":"ref13","first-page":"82:1","article-title":"Narcissus: Correct-by-construction derivation of decoders and encoders from binary formats","volume":"3","author":"Delaware","year":"2019","journal-title":"PACMPL"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294105"},{"issue":"3","key":"ref15","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1007\/s10817-017-9429-1","article-title":"Bidirectional grammars for machine-code decoding and encoding","volume":"60","author":"Tan","year":"2018","journal-title":"J. Autom. Reasoning"},{"issue":"5","key":"ref16","doi-asserted-by":"crossref","first-page":"552","DOI":"10.1017\/S095679681300018X","article-title":"Idris, a general-purpose dependently typed programming language: Design and implementation","volume":"23","author":"Brady","year":"2013","journal-title":"J. Funct. Program"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-45279-1_7"},{"key":"ref18","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/978-3-642-03359-9_6","article-title":"A brief overview of Agda-A functional language with dependent types","volume-title":"Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings","volume":"5674","author":"Bove"},{"issue":"2","key":"ref19","first-page":"1","article-title":"Certified context-free parsing: A formalisation of Valiant\u2019s algorithm in agda","volume":"12","author":"Bernardy","year":"2016","journal-title":"Logical Methods in Computer Science"},{"key":"ref20","first-page":"24:1","article-title":"A verified LL(1) parser generator","volume-title":"10th International Conference onInteractive Theorem Proving, ITp 2019, September 9-12, 2019, Portland, OR, USA., ser. LIPIcs","volume":"141","author":"Lasser"},{"key":"ref21","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","article-title":"Interactive Theorem Proving and Program Development","author":"Bertot","year":"2004"},{"issue":"2","key":"ref22","first-page":"1","article-title":"TRX: A formally verified parser interpreter","volume":"7","author":"Koprowski","year":"2011","journal-title":"Logical Methods in Computer Science"},{"key":"ref23","first-page":"179","article-title":"Cakeml: A verified implementation of ML","volume-title":"The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914, San Diego, CA, USA, January 20-21, 2014","author":"Kumar"},{"key":"ref24","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","article-title":"A brief overview of HOL4","volume-title":"Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings","volume":"5170","author":"Slind"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_12"},{"key":"ref26","first-page":"103","article-title":"Packrat parsers can support left recursion","volume-title":"Proceedings of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, ser. PEPM \u201908","author":"Warth"},{"key":"ref27","first-page":"177","article-title":"Left recursion in parsing expression grammars","volume-title":"Science of Computer Programming","volume":"96","author":"Medeiros"}],"event":{"name":"2024 IEEE Security and Privacy Workshops (SPW)","start":{"date-parts":[[2024,5,23]]},"location":"San Francisco, CA, USA","end":{"date-parts":[[2024,5,23]]}},"container-title":["2024 IEEE Security and Privacy Workshops (SPW)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/10579499\/10579500\/10579503.pdf?arnumber=10579503","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,7]],"date-time":"2024-07-07T05:36:06Z","timestamp":1720330566000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10579503\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,23]]},"references-count":27,"URL":"https:\/\/doi.org\/10.1109\/spw63631.2024.00022","relation":{},"subject":[],"published":{"date-parts":[[2024,5,23]]}}}