Partial derivative automata formalized in Coq
- Almeida, José Bacelar
- Moreira, Nelma
- Pereira, David
- Sousa, Simão Melo de
Publication date
January 2011
DOI Publisher
Springer Science and Business Media LLC ISSN
0302-9743 Journal
0302-9743 Citation count (estimate)
13Abstract
In this paper we present a computer assisted proof of the correctness of a partial derivative automata construction from a regular expression within the Coq proof assistant. This proof is part of a for- malization of Kleene algebra and regular languages in Coq towards their usage in program certification.Fundação para a Ciência e Tecnologia (FCT) Program POSI, RESCUE (PTDC/EIA/65862/2006), SFRH/BD/33233/2007
Add to ORKG