logo

SCIENCE CHINA Information Sciences, Volume 61, Issue 2: 028101(2018) https://doi.org/10.1007/s11432-017-9155-x

The verification of conversion algorithms between finite automata

More info
  • ReceivedMay 29, 2017
  • AcceptedJun 29, 2017
  • PublishedNov 17, 2017

Abstract

There is no abstract available for this article.


Acknowledgment

This work was supported by Beijing Natural Science Foundation (Grant No. 4164092) and Fundamental Research Funds for Central Universities (Grant No. BLX2015-17).


Supplement

Appendixes A and B.


References

[1] Filliâtre J C. Finite Auotmata Theory in Coq: a Constructive Proof of Kleenes Theorem. Research Report 97-04, LIP-ENS Lyon. 1997. Google Scholar

[2] Braibant T, Pous D. An efficient Coq tactic for deciding Kleene algebras. In: Proceedings of International Conference on Interactive Theorem Proving, Edinburgh, 2010. 163--178. Google Scholar

[3] Lammich P, Tuerk T. Applying data refinement for monadic programs to Hopcrofts algorithm. In: Proceedings of International Conference on Interactive Theorem Proving, New Jersey, 2012. 166--182. Google Scholar

[4] Paulson L C. A Formalisation of finite automata using hereditarily finite sets. In: Proceedings of CADE-25-International Conference on Automated Deduction, Berlin, 2015. 231--245. Google Scholar

[5] Lammich P, Lochbihler A. The isabelle collections framework. In: Proceedings of International Conference on Interactive Theorem Proving, New Jersey, 2010. 339--354. Google Scholar

[6] Esparza J. Automata Theory: an Algorithmic Approach. 2016. https://www7.in.tum.de/~esparza/autoskript.pdf. Google Scholar

Copyright 2019 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有

京ICP备18024590号-1