CertiStr: A Certified String Solver
summary
CertiStr is a certified solver for strings with concatenation and regular constraints, proven correct in Isabelle/HOL-certified OCaml extraction and implemented using symbolic automata with interval transitions. It decides sat/unsat/unknown via a forward-propagation over symbolic automata algorithm that guarantees termination for acyclic concatenation dependencies and implements automata operations (concatenate, product, rename). Evaluation on the Kaluza benchmark shows the fragment coverage is 80.4% and CertiStr solves 83.5% solved within 60s; backreferences are not currently supported.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:15String Constraint
- 2:02Motivation
- 2:55Theory of the String
- 3:43Forward Propagation
- 5:20While Loop
- 6:23correctness
- 8:02tree property
- 10:16Formalization Example
- 12:22Implementation Level
- 12:56Evaluation
- 14:10Summary
related talks
25mCertified Symbolic Finite Transducers: Formalization and Applications to String Analysis
58mAutomating Relational Verification of Infinite-State Programs
28mProving Memory Access Violations in Isabelle/HOL
21mFormal Methods for Everyone: Practical Tools for Computer-Aided Reasoning
25mASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER
16mCerisier: A Program Logic for Attestation in a Capability Machine
06mFormal Verification with the Certora Prover
25mVerifying LLM powered Code Transformations with Equivalence Checking