Checking regular expressions in cvc5 proofs

DOI10.1007/978-3-032-32589-1_16MaRDI QIDQ7411170zbMATH OpenFDO

Authors Ofec Israel, Yoni Zohar, Andrew Reynolds, S. Hitarth, Bruno Dutertre, Clark Barrett, Cesare Tinelli

Publication date 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-032-32589-1_16

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format
• Derivatives of Regular Expressions
• Programming Techniques: Regular expression search algorithm
• Regular-expression derivatives re-examined

This page was built for publication: Checking regular expressions in cvc5 proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7411170)