TY - GEN
T1 - Formal proofs for automata and sticker systems
AU - Tanaka, Hisaharu
AU - Sakashita, Issei
AU - Inokuchi, Shuichi
AU - Mizoguchi, Yoshihiro
PY - 2013
Y1 - 2013
N2 - We implemented operations appeared in the theory of automata using the Coq proof-assistant. A language which contains infinite elements is defined using ssreflect (a Small Scale Reflection Extension for the Coq system). We also implemented the modules for sticker systems. Pu{a}un and Rozenberg introduced a concrete method to transform an automaton to a sticker system in 1998. One of our aims is to present formal proofs of the correctness of their transformation. We modified some of their definitions to improve their insufficient results. We note that all of our formulation are written in Coq and we show some examples of machine-checkable proofs.
AB - We implemented operations appeared in the theory of automata using the Coq proof-assistant. A language which contains infinite elements is defined using ssreflect (a Small Scale Reflection Extension for the Coq system). We also implemented the modules for sticker systems. Pu{a}un and Rozenberg introduced a concrete method to transform an automaton to a sticker system in 1998. One of our aims is to present formal proofs of the correctness of their transformation. We modified some of their definitions to improve their insufficient results. We note that all of our formulation are written in Coq and we show some examples of machine-checkable proofs.
UR - http://www.scopus.com/inward/record.url?scp=84894207259&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84894207259&partnerID=8YFLogxK
U2 - 10.1109/CANDAR.2013.100
DO - 10.1109/CANDAR.2013.100
M3 - Conference contribution
AN - SCOPUS:84894207259
SN - 9781479927951
T3 - Proceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013
SP - 563
EP - 566
BT - Proceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013
T2 - 2013 1st International Symposium on Computing and Networking, CANDAR 2013
Y2 - 4 December 2013 through 6 December 2013
ER -