Formal proofs for automata and sticker systems

Hisaharu Tanaka, Issei Sakashita, Shuichi Inokuchi, Yoshihiro Mizoguchi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish
Title of host publicationProceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013
Pages563-566
Number of pages4
DOIs
Publication statusPublished - Dec 1 2013
Event2013 1st International Symposium on Computing and Networking, CANDAR 2013 - Matsuyama, Ehime, Japan
Duration: Dec 4 2013Dec 6 2013

Publication series

NameProceedings - 2013 1st International Symposium on Computing and Networking, CANDAR 2013

Other

Other2013 1st International Symposium on Computing and Networking, CANDAR 2013
CountryJapan
CityMatsuyama, Ehime
Period12/4/1312/6/13

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications

Cite this

Tanaka, H., Sakashita, I., Inokuchi, S., & Mizoguchi, Y. (2013). Formal proofs for automata and sticker systems. In 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).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Tanaka, H, Sakashita, I, Inokuchi, S & Mizoguchi, Y 2013, Formal proofs for automata and sticker systems. in 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, Japan, 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. In 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

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 -