Partial Derivative Automata Formalized in Coq
- Citation:
- Almeida JB, Moreira N, Pereira D, Sousa SM. 2010. Partial Derivative Automata Formalized in Coq. 15th International Conference on Implementation and Application of Automata - CIAA - Revised Selected Papers . :59-68.
Date Presented:
AugustAbstract:
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 formalization of Kleene algebra and regular languages in Coq towards their usage in program certification.
Citation Key:
DBLP:conf/wia/AlmeidaMPS10DOI:
10.1007/978-3-642-18098-9_7
Tags
- Coq (2)
- formalization (1)
- language closure (1)
- MEE-CBC (1)
- Pumping Lemma (2)
- s2n library (1)
- timing attacks (1)
Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.