Symbolic Boolean Derivatives for Efficiently Solving Extended Regular Expression Constraints
The manipulation of raw string data is ubiquitous in security-critical software, and verification of such software relies on efficiently solving string and regular expression constraints via SMT. However, the typical case of Boolean combinations of regular expression constraints exposes blowup in existing techniques. To address solvability of such constraints, we propose a new theory of derivatives of symbolic extended regular expressions (extended meaning that complement and intersection are incorporated), and show how to apply this theory to obtain more efficient decision procedures. Our implementation of these ideas, built on top of Z3, matches or outperforms state-of-the-art solvers on standard and handwritten benchmarks, showing particular benefits on examples with Boolean combinations.
Our work is the first formalization of derivatives of regular expressions which both handles intersection and complement and works symbolically over an arbitrary character theory. It unifies existing approaches involving derivatives of extended regular expressions, alternating automata and Boolean automata by lifting them to a common symbolic platform. It relies on a parsimonious augmentation of regular expressions: a construct for symbolic conditionals is shown to be sufficient to obtain relevant closure properties for derivatives over extended regular expressions.
Fri 22 OctDisplayed time zone: Central Time (US & Canada) change
13:50 - 15:10 | PLDI 2021 Papers 5SIGPLAN Papers at Zurich F Chair(s): Feras Saad Massachusetts Institute of Technology | ||
13:50 15mTalk | Repairing Serializability Bugs in Distributed Database Programs via Automated Schema Refactoring SIGPLAN Papers Kia Rahmani Purdue University, Kartik Nagar IIT Madras, Benjamin Delaware Purdue University, Suresh Jagannathan Purdue University | ||
14:05 15mTalk | Scooter & Sidecar: A domain-specific approach to writing secure migrations SIGPLAN Papers John Renner University of California at San Diego, USA, Alex Sanchez-Stern University of California at San Diego, Fraser Brown Stanford University, USA, Sorin Lerner University of California at San Diego, Deian Stefan University of California at San Diego, USA | ||
14:20 15mTalk | Symbolic Boolean Derivatives for Efficiently Solving Extended Regular Expression Constraints SIGPLAN Papers Caleb Stanford University of Pennsylvania, Margus Veanes Microsoft, Nikolaj Bjørner Microsoft Research | ||
14:35 15mTalk | Filling Typed Holes with Live GUIs SIGPLAN Papers Cyrus Omar University of Michigan, David Moon University of Michigan, Andrew Blinn University of Michigan, Ian Voysey Carnegie Mellon University, Nick Collins University of Chicago, Ravi Chugh University of Chicago | ||
14:50 20mLive Q&A | Discussion, Questions and Answers SIGPLAN Papers |