Partial Derivative Automata Formalized in Coq

• Type: Article in International Conference Proceedings Book
• Date: 2011

Authors

Jose Bacelar Almeida (Author) Other; Nelma Moreira (Author) FCUP; David Pereira (Author) Other; Simao Melo de Sousa (Author) Other

Conference proceedings International

Title: Implementation and Application of Automata, 17th International Conference (CIAA 2012)

Pages: 59-68

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

Porto, 17-20, Julho, 2012

Indexing

ISI Web of Knowledge - 3 Citations

Scopus - 14 Citations

Scientific classification

FOS: Natural sciences > Computer and information sciences

Other information

Authenticus ID: 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.

Language: English

Type (Professor's evaluation): Scientific

No. of pages: 10