Morpheus: Automated Safety Verification of Data-dependent Parser Combinator Programs
Parser combinators are a well-known mechanism used for the compositional construction of parsers, and have shown to be particularly useful in writing parsers for rich grammars with data-dependencies and global state. Verifying applications written using them, however, has proven to be challenging in large part because of the inherently effectful nature of the parsers being composed and the difficulty in reasoning about the arbitrarily rich data-dependent semantic actions that can be associated with parsing actions. In this paper, we address these challenges by defining a parser combinator framework called Morpheus equipped with abstractions for defining composable effects tailored for parsing and semantic actions, and a rich specification language used to define safety properties over the constituent parsers comprising a program. Even though its abstractions yield many of the same expressivity benefits as other parser combinator systems, Morpheus is carefully engineered to yield a substantially more tractable automated verification pathway. We demonstrate its utility in verifying a number of realistic, challenging parsing applications, including several cases that involve non-trivial data-dependent relations.
Fri 21 JulDisplayed time zone: Pacific Time (US & Canada) change
10:30 - 12:00 | ECOOP 7: Verification and TestingResearch Papers at Amazon Auditorium (Gates G20) Chair(s): Wenxi Wang University of Texas at Austin | ||
10:30 15mTalk | On using VeriFast, VerCors, Plural, and KeY to check object usage Research Papers João Mota NOVA School of Science and Technology, António Ravara NOVA LINCS & FCT, NOVA University of Lisbon, Marco Giunti NOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa DOI | ||
10:45 15mTalk | Exact Separation Logic Research Papers Petar Maksimović Imperial College London, UK, Caroline Cronjäger Ruhr-Universität Bochum, Andreas Lööw Imperial College London, Julian Sutherland Imperial College London, Philippa Gardner Imperial College London DOI Pre-print | ||
11:00 15mTalk | Morpheus: Automated Safety Verification of Data-dependent Parser Combinator Programs Research Papers DOI | ||
11:15 15mTalk | Constraint Based Compiler Optimization for Energy Harvesting Applications Research Papers DOI | ||
11:30 15mTalk | Dynamic Determinacy Race Detection for Task-Parallel Programs with Promises Research Papers Feiyang Jin Georgia Institute of Technology, Lechen Yu Georgia Institute of Technology, Tiago Cogumbreiro University of Massachusetts Boston, Vivek Sarkar Georgia Institute of Technology, Jun Shirako Georgia Institute of Technology DOI | ||
11:45 15mTalk | On Leveraging Tests to Infer Nullable Annotations Research Papers Jens Dietrich Victoria University of Wellington, David J. Pearce ConsenSys, Mahin Chandramohan Oracle Labs DOI |