26 citations · 37 across the 6 of their papers we have counts for
6 papers
On the computational complexity of JavaScript regex matching
Victor Deng, Aurèle Barrière, Clément Pit-Claudel
Despite widespread use, the complexity of the matching problem for modern regular expressions languages remains unclear. Previous work proved that an idealized regular expression l…
Formal Verification for JavaScript Regular Expressions: a Proven Semantics and its Applications (Extended Version)
Aurèle Barrière, Victor Deng, Clément Pit-Claudel
We present the first mechanized, succinct, practical, complete, and proven-faithful semantics for a modern regular expression language with backtracking semantics. We ensure its fa…
A Coq Mechanization of JavaScript Regular Expression Semantics
Noé De Santo, Aurèle Barrière, Clément Pit-Claudel
We present an executable, proven-safe, faithful, and future-proof Coq mechanization of JavaScript regular expression (regex) matching, as specified by the latest published edition…
Linear Matching of JavaScript Regular Expressions
Aurèle Barrière, Clément Pit-Claudel
Modern regex languages have strayed far from well-understood traditional regular expressions: they include features that fundamentally transform the matching problem. In exchange f…
Formally Verified Native Code Generation in an Effectful JIT -- or: Turning the CompCert Backend into a Formally Verified JIT Compiler
Aurèle Barrière, Sandrine Blazy, David Pichardie
Modern Just-in-Time compilers (or JITs) typically interleave several mechanisms to execute a program. For faster startup times and to observe the initial behavior of an execution,…
Changing Observations in Epistemic Temporal Logic
Aurèle Barrière, Bastien Maubert, Aniello Murano +1
We study dynamic changes of agents' observational power in logics of knowledge and time. We consider CTL*K, the extension of CTL* with knowledge operators, and enrich it with a new…