This paper presents a toolbox implemented in Coq and dedicated to the specification and verification of synchronous sequential devices. The use of Coq co-inductive types underpins our methodology and leads to elegant and uniform descriptions of the circuits and their behaviours as well as clear and short proofs. An application to a non trivial circuit is given as an illustration.
CITATION STYLE
Coupet—Grimal, S., & Jakubiec, L. (1999). Hardware verification using co-induction in COQ. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1690, pp. 91–108). Springer Verlag. https://doi.org/10.1007/3-540-48256-3_7
Mendeley helps you to discover research relevant for your work.