3 papers
cs.LO2026
A Deeper Look at Depth: Stable Generation Accounting for Quantifier Reasoning
Can Cebeci, Nikolaj Bjørner, George Candea +1
SMT solvers make automated verification convenient. At the same time, solvers suffer from instability, whereby seemingly inconsequential changes to the input may cause a previously…
cs.PL2026
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…
cs.LO2025
Verified and Optimized Implementation of Orthologic Proof Search
Simon Guilloud, Clément Pit-Claudel
We report on the development of an optimized and verified decision procedure for orthologic equalities and inequalities. This decision procedure is quadratic-time and is used as a…