Formal proofs for automata and sticker systems

Hisaharu Tanaka, Issei Sakashita, Shuichi Inokuchi, Yoshihiro Mizoguchi

研究成果: 著書/レポートタイプへの貢献会議での発言

抄録

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.

元の言語英語
ホスト出版物のタイトルProceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013
ページ563-566
ページ数4
DOI
出版物ステータス出版済み - 12 1 2013
イベント2013 1st International Symposium on Computing and Networking, CANDAR 2013 - Matsuyama, Ehime, 日本
継続期間: 12 4 201312 6 2013

出版物シリーズ

名前Proceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013

その他

その他2013 1st International Symposium on Computing and Networking, CANDAR 2013
日本
Matsuyama, Ehime
期間12/4/1312/6/13

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications

これを引用

Tanaka, H., Sakashita, I., Inokuchi, S., & Mizoguchi, Y. (2013). Formal proofs for automata and sticker systems. : Proceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013 (pp. 563-566). [6726962] (Proceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013). https://doi.org/10.1109/CANDAR.2013.100

Formal proofs for automata and sticker systems. / Tanaka, Hisaharu; Sakashita, Issei; Inokuchi, Shuichi; Mizoguchi, Yoshihiro.

Proceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013. 2013. p. 563-566 6726962 (Proceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013).

研究成果: 著書/レポートタイプへの貢献会議での発言

Tanaka, H, Sakashita, I, Inokuchi, S & Mizoguchi, Y 2013, Formal proofs for automata and sticker systems. : Proceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013., 6726962, Proceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013, pp. 563-566, 2013 1st International Symposium on Computing and Networking, CANDAR 2013, Matsuyama, Ehime, 日本, 12/4/13. https://doi.org/10.1109/CANDAR.2013.100
Tanaka H, Sakashita I, Inokuchi S, Mizoguchi Y. Formal proofs for automata and sticker systems. : Proceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013. 2013. p. 563-566. 6726962. (Proceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013). https://doi.org/10.1109/CANDAR.2013.100
Tanaka, Hisaharu ; Sakashita, Issei ; Inokuchi, Shuichi ; Mizoguchi, Yoshihiro. / Formal proofs for automata and sticker systems. Proceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013. 2013. pp. 563-566 (Proceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013).
@inproceedings{3e20525f597049b48966d172b4f95855,
title = "Formal proofs for automata and sticker systems",
abstract = "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.",
author = "Hisaharu Tanaka and Issei Sakashita and Shuichi Inokuchi and Yoshihiro Mizoguchi",
year = "2013",
month = "12",
day = "1",
doi = "10.1109/CANDAR.2013.100",
language = "English",
isbn = "9781479927951",
series = "Proceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013",
pages = "563--566",
booktitle = "Proceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013",

}

TY - GEN

T1 - Formal proofs for automata and sticker systems

AU - Tanaka, Hisaharu

AU - Sakashita, Issei

AU - Inokuchi, Shuichi

AU - Mizoguchi, Yoshihiro

PY - 2013/12/1

Y1 - 2013/12/1

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

ER -