Wed 19 Jan 2022 11:35 - 12:00 at Salon I - Automated Verification Chair(s): Roberto Giacobazzi

Regular expressions are a classical concept in formal language theory. Regular expressions in programming languages (RegEx) such as JavaScript, feature non-standard semantics of operators (e.g. greedy/lazy Kleene star), as well as additional features such as capturing groups and references. While symbolic execution of programs containing RegExes appeals to string solvers natively supporting important features of RegEx, such a string solver is hitherto missing. In this paper, we propose the first string theory and string solver that natively provides such support. The key idea of our string solver is to introduce a new automata model, called prioritized streaming string transducers (PSST), to formalize the semantics of RegEx-dependent string functions. PSSTs combine priorities, which have previously been introduced in prioritized finite-state automata to capture greedy/lazy semantics, with string variables as in streaming string transducers to model capturing groups. We validate the consistency of the formal semantics with the actual JavaScript semantics by extensive experiments. Furthermore, to solve the string constraints, we show that PSSTs enjoy nice closure and algorithmic properties, in particular, the regularity-preserving property (i.e., pre-images of regular constraints under PSSTs are regular), and introduce a sound sequent calculus that exploits these properties and performs propagation of regular constraints by means of taking post-images or pre-images. Although the satisfiability of the string constraint language is generally undecidable, we show that our approach is complete for the so-called straight-line fragment. We evaluate the performance of our string solver on over 195000 string constraints generated from an open-source RegEx library. The experimental results show the efficacy of our approach, drastically improving the existing methods (via symbolic execution) in both precision and efficiency.

Wed 19 Jan

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

10:20 - 12:00
Automated VerificationPOPL at Salon I
Chair(s): Roberto Giacobazzi University of Verona
10:20
25m
Research paper
Software Model-Checking as Cyclic-Proof SearchRemote
POPL
Takeshi Tsukada Chiba University, Hiroshi Unno University of Tsukuba; RIKEN AIP
DOI Media Attached
10:45
25m
Research paper
Induction Duality: Primal-Dual Search for InvariantsRemote
POPL
Oded Padon VMware Research; Stanford University, James R. Wilcox Certora, Jason R. Koenig Stanford University, Kenneth L. McMillan University of Texas at Austin, Alex Aiken Stanford University
DOI Media Attached
11:10
25m
Research paper
Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive FunctionsRemote
POPL
Hari Govind V K University of Waterloo, Sharon Shoham Tel Aviv University, Arie Gurfinkel University of Waterloo
DOI Media Attached
11:35
25m
Research paper
Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and VariablesRemote
POPL
Taolue Chen Birkbeck University of London, Alejandro Flores Lamas Royal Holloway University of London, Matthew Hague Royal Holloway University of London, Zhilei Han Tsinghua University, Denghang Hu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Shuanglong Kan TU Kaiserslautern, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Philipp Ruemmer Uppsala University, Zhilin Wu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences
DOI Media Attached