Specification and Verification of Invariant Properties of Transition Systems

Daniel Mircea Gaina, Ionut Tutu, Adrian Riesco

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

抄録

Transition systems provide a natural way to specify and reason about the behaviour of discrete systems, and in particular about the computations that they may perform. This paper advances a verification method for transition systems whose reachable states are described explicitly by membership axioms. The proof technique is implemented in the Constructor-based Inductive Theorem Prover (CITP), a proof management tool built on top of a variation of conditional equational logic enhanced with many modern features. This approach complements the so-called OTS method, a verification procedure for observational transition systems that is already implemented in CITP.

元の言語英語
ホスト出版物のタイトルProceedings - 25th Asia-Pacific Software Engineering Conference, APSEC 2018
出版者IEEE Computer Society
ページ99-108
ページ数10
ISBN(電子版)9781728119700
DOI
出版物ステータス出版済み - 5 21 2019
イベント25th Asia-Pacific Software Engineering Conference, APSEC 2018 - Nara, 日本
継続期間: 12 4 201812 7 2018

出版物シリーズ

名前Proceedings - Asia-Pacific Software Engineering Conference, APSEC
2018-December
ISSN(印刷物)1530-1362

会議

会議25th Asia-Pacific Software Engineering Conference, APSEC 2018
日本
Nara
期間12/4/1812/7/18

Fingerprint

Specifications

All Science Journal Classification (ASJC) codes

  • Software

これを引用

Gaina, D. M., Tutu, I., & Riesco, A. (2019). Specification and Verification of Invariant Properties of Transition Systems. : Proceedings - 25th Asia-Pacific Software Engineering Conference, APSEC 2018 (pp. 99-108). [8719485] (Proceedings - Asia-Pacific Software Engineering Conference, APSEC; 巻数 2018-December). IEEE Computer Society. https://doi.org/10.1109/APSEC.2018.00024

Specification and Verification of Invariant Properties of Transition Systems. / Gaina, Daniel Mircea; Tutu, Ionut; Riesco, Adrian.

Proceedings - 25th Asia-Pacific Software Engineering Conference, APSEC 2018. IEEE Computer Society, 2019. p. 99-108 8719485 (Proceedings - Asia-Pacific Software Engineering Conference, APSEC; 巻 2018-December).

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

Gaina, DM, Tutu, I & Riesco, A 2019, Specification and Verification of Invariant Properties of Transition Systems. : Proceedings - 25th Asia-Pacific Software Engineering Conference, APSEC 2018., 8719485, Proceedings - Asia-Pacific Software Engineering Conference, APSEC, 巻. 2018-December, IEEE Computer Society, pp. 99-108, 25th Asia-Pacific Software Engineering Conference, APSEC 2018, Nara, 日本, 12/4/18. https://doi.org/10.1109/APSEC.2018.00024
Gaina DM, Tutu I, Riesco A. Specification and Verification of Invariant Properties of Transition Systems. : Proceedings - 25th Asia-Pacific Software Engineering Conference, APSEC 2018. IEEE Computer Society. 2019. p. 99-108. 8719485. (Proceedings - Asia-Pacific Software Engineering Conference, APSEC). https://doi.org/10.1109/APSEC.2018.00024
Gaina, Daniel Mircea ; Tutu, Ionut ; Riesco, Adrian. / Specification and Verification of Invariant Properties of Transition Systems. Proceedings - 25th Asia-Pacific Software Engineering Conference, APSEC 2018. IEEE Computer Society, 2019. pp. 99-108 (Proceedings - Asia-Pacific Software Engineering Conference, APSEC).
@inproceedings{c68bc696df80430d819c81cfcc7a7a46,
title = "Specification and Verification of Invariant Properties of Transition Systems",
abstract = "Transition systems provide a natural way to specify and reason about the behaviour of discrete systems, and in particular about the computations that they may perform. This paper advances a verification method for transition systems whose reachable states are described explicitly by membership axioms. The proof technique is implemented in the Constructor-based Inductive Theorem Prover (CITP), a proof management tool built on top of a variation of conditional equational logic enhanced with many modern features. This approach complements the so-called OTS method, a verification procedure for observational transition systems that is already implemented in CITP.",
author = "Gaina, {Daniel Mircea} and Ionut Tutu and Adrian Riesco",
year = "2019",
month = "5",
day = "21",
doi = "10.1109/APSEC.2018.00024",
language = "English",
series = "Proceedings - Asia-Pacific Software Engineering Conference, APSEC",
publisher = "IEEE Computer Society",
pages = "99--108",
booktitle = "Proceedings - 25th Asia-Pacific Software Engineering Conference, APSEC 2018",
address = "United States",

}

TY - GEN

T1 - Specification and Verification of Invariant Properties of Transition Systems

AU - Gaina, Daniel Mircea

AU - Tutu, Ionut

AU - Riesco, Adrian

PY - 2019/5/21

Y1 - 2019/5/21

N2 - Transition systems provide a natural way to specify and reason about the behaviour of discrete systems, and in particular about the computations that they may perform. This paper advances a verification method for transition systems whose reachable states are described explicitly by membership axioms. The proof technique is implemented in the Constructor-based Inductive Theorem Prover (CITP), a proof management tool built on top of a variation of conditional equational logic enhanced with many modern features. This approach complements the so-called OTS method, a verification procedure for observational transition systems that is already implemented in CITP.

AB - Transition systems provide a natural way to specify and reason about the behaviour of discrete systems, and in particular about the computations that they may perform. This paper advances a verification method for transition systems whose reachable states are described explicitly by membership axioms. The proof technique is implemented in the Constructor-based Inductive Theorem Prover (CITP), a proof management tool built on top of a variation of conditional equational logic enhanced with many modern features. This approach complements the so-called OTS method, a verification procedure for observational transition systems that is already implemented in CITP.

UR - http://www.scopus.com/inward/record.url?scp=85066784694&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85066784694&partnerID=8YFLogxK

U2 - 10.1109/APSEC.2018.00024

DO - 10.1109/APSEC.2018.00024

M3 - Conference contribution

AN - SCOPUS:85066784694

T3 - Proceedings - Asia-Pacific Software Engineering Conference, APSEC

SP - 99

EP - 108

BT - Proceedings - 25th Asia-Pacific Software Engineering Conference, APSEC 2018

PB - IEEE Computer Society

ER -