Write a Blog >>
PLDI 2021
Sun 20 - Sat 26 June 2021 PLDI
Wed 23 Jun 2021 09:15 - 09:20 at PLDI-B - Talks 1B: Verification
Wed 23 Jun 2021 21:15 - 21:20 at PLDI-B - Talks 1B: Verification

Parsers are security-critical components of many software systems, and verified parsing therefore has a key role to play in secure software design. However, existing verified parsers for context-free grammars are limited in their expressiveness, termination properties, or performance characteristics. They are only compatible with a restricted class of grammars, they are not guaranteed to terminate on all inputs, or they are not designed to be performant on grammars for real-world programming languages and data formats.

In this work, we present CoStar, a verified parser that addresses these limitations. The parser is implemented with the Coq Proof Assistant and is based on the ALL(*) parsing algorithm. CoStar is sound and complete for all non-left-recursive grammars; it produces a correct parse tree for its input whenever such a tree exists, and it correctly detects ambiguous inputs. CoStar also provides strong termination guarantees; it terminates without error on all inputs when applied to a non-left-recursive grammar. Finally, CoStar achieves linear-time performance on a range of unambiguous grammars for commonly used languages and data formats.

Wed 23 Jun

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 09:35
Talks 1B: VerificationPLDI at PLDI-B +12h
09:00
5m
Talk
Proof Repair across Type Equivalences
PLDI
Talia Ringer University of Illinois at Urbana-Champaign, RanDair Porter University of Washington, Nathaniel Yazdani Northeastern University, John Leo Halfaya Research, Dan Grossman University of Washington
DOI
09:05
5m
Talk
Zooid: A DSL for Certified Multiparty Computation: From Mechanised Metatheory to Certified Multiparty Processes
PLDI
David Castro-Perez University of Kent, Francisco Ferreira Imperial College London, Lorenzo Gheri Imperial College London, Nobuko Yoshida Imperial College London
DOI
09:10
5m
Talk
Beyond the Elementary Representations of Program Invariants over Algebraic Data Types
PLDI
Yurii Kostyukov St. Petersburg State University; JetBrains Research, Dmitry Mordvinov St. Petersburg State University; JetBrains Research, Grigory Fedyukovich Florida State University
DOI
09:15
5m
Talk
CoStar: A Verified ALL(*) Parser
PLDI
Sam Lasser Tufts University, Chris Casinghino Draper, Kathleen Fisher Tufts University, Cody Roux Draper
DOI
09:20
5m
Talk
Symbolic Boolean Derivatives for Efficiently Solving Extended Regular Expression Constraints
PLDI
Caleb Stanford University of Pennsylvania, Margus Veanes Microsoft Research, Nikolaj Bjørner Microsoft Research
DOI
09:25
5m
Talk
Integration Verification across Software and Hardware for a Simple Embedded System
PLDI
Andres Erbsen Massachusetts Institute of Technology, Samuel Gruetter Massachusetts Institute of Technology, Joonwon Choi Massachusetts Institute of Technology, Clark Wood Massachusetts Institute of Technology, Adam Chlipala Massachusetts Institute of Technology
DOI
09:30
5m
Talk
Satisfiability Modulo Ordering Consistency Theory for Multi-threaded Program Verification
PLDI
Fei He Tsinghua University, Zhihang Sun Tsinghua University, Hongyu Fan Tsinghua University
DOI
21:00 - 21:35
Talks 1B: VerificationPLDI at PLDI-B
21:00
5m
Talk
Proof Repair across Type Equivalences
PLDI
Talia Ringer University of Illinois at Urbana-Champaign, RanDair Porter University of Washington, Nathaniel Yazdani Northeastern University, John Leo Halfaya Research, Dan Grossman University of Washington
DOI
21:05
5m
Talk
Zooid: A DSL for Certified Multiparty Computation: From Mechanised Metatheory to Certified Multiparty Processes
PLDI
David Castro-Perez University of Kent, Francisco Ferreira Imperial College London, Lorenzo Gheri Imperial College London, Nobuko Yoshida Imperial College London
DOI
21:10
5m
Talk
Beyond the Elementary Representations of Program Invariants over Algebraic Data Types
PLDI
Yurii Kostyukov St. Petersburg State University; JetBrains Research, Dmitry Mordvinov St. Petersburg State University; JetBrains Research, Grigory Fedyukovich Florida State University
DOI
21:15
5m
Talk
CoStar: A Verified ALL(*) Parser
PLDI
Sam Lasser Tufts University, Chris Casinghino Draper, Kathleen Fisher Tufts University, Cody Roux Draper
DOI
21:20
5m
Talk
Symbolic Boolean Derivatives for Efficiently Solving Extended Regular Expression Constraints
PLDI
Caleb Stanford University of Pennsylvania, Margus Veanes Microsoft Research, Nikolaj Bjørner Microsoft Research
DOI
21:25
5m
Talk
Integration Verification across Software and Hardware for a Simple Embedded System
PLDI
Andres Erbsen Massachusetts Institute of Technology, Samuel Gruetter Massachusetts Institute of Technology, Joonwon Choi Massachusetts Institute of Technology, Clark Wood Massachusetts Institute of Technology, Adam Chlipala Massachusetts Institute of Technology
DOI
21:30
5m
Talk
Satisfiability Modulo Ordering Consistency Theory for Multi-threaded Program Verification
PLDI
Fei He Tsinghua University, Zhihang Sun Tsinghua University, Hongyu Fan Tsinghua University
DOI