Abstract
We describe and verify an elegant equivalence checker for regular expressions. It works by constructing a bisimulation relation between (derivatives of) regular expressions. By mapping regular expressions to binary relations, an automatic and complete proof method for (in)equalities of binary relations over union, composition and (reflexive) transitive closure is obtained. The verification is carried out in the theorem prover Isabelle/HOL, yielding a practically useful decision procedure.
| Original language | English |
|---|---|
| Pages (from-to) | 95-106 |
| Number of pages | 12 |
| Journal | Journal of Automated Reasoning |
| Volume | 49 |
| Issue number | 1 |
| DOIs | |
| State | Published - Jun 2012 |
Keywords
- Decision procedure
- Isabelle/HOL
- Regular expressions