Partial Derivative Automata Formalized in Coq

• Tipo: Artigo em Livro de Atas de Conferência Internacional
• Data: 2011

Autores

Jose Bacelar Almeida (Autor) Outra; Nelma Moreira (Autor) FCUP; David Pereira (Autor) Outra; Simao Melo de Sousa (Autor) Outra

Ata de Conferência Internacional

Título: Implementation and Application of Automata, 17th International Conference (CIAA 2012)

Páginas: 59-68

17th International Conference on Implementation and Application of Automata (CIAA)

Porto, 17-20, Julho, 2012

Indexação

ISI Web of Knowledge - 3 Citações

Scopus - 14 Citações

Classificação Científica

FOS: Ciências exactas e naturais > Ciências da computação e da informação

Outras Informações

ID Authenticus: P-002-XJV

DOI: 10.1007/978-3-642-18098-9_7

Abstract (EN): 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. Tins proof is part of a formalization of Kleene algebra and regular languages in Coq towards their usage in program certification.

Idioma: Inglês

Tipo (Avaliação Docente): Científica

Nº de páginas: 10