Technische Universität München Institut für Informatik Theorem Proving Group |     Alexander Krauss

Alexander Krauss (TUM, QAware GmbH) and Tobias Nipkow (TUM)

Formalized Regular Expression Equivalence and Relation Algebra (in Isabelle/HOL)

Material for my talk at RAMiCS 2012

Abstract: We present the Isabelle formalization of an elegant equivalence checker for regular expressions. It works by constructing a bisimulation relation between (derivatives of) regular expressions. By mapping 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, which adds a practically useful decision procedure to the automation toolbox of Isabelle/HOL.

[ Theory sources (tar.gz) | Slides (pdf) ]

See also the paper on the same topic and the entry Regular_Sets in the Archive of Formal Proofs