Specification and Verification of Invariant Properties of Transition Systems

Daniel Gaina, Ionut Tutu, Adrian Riesco

研究成果: Chapter in Book/Report/Conference proceedingConference contribution

4 被引用数 (Scopus)

抄録

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
出版ステータス出版済み - 7 2 2018
イベント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
Country日本
CityNara
Period12/4/1812/7/18

All Science Journal Classification (ASJC) codes

  • Software

フィンガープリント 「Specification and Verification of Invariant Properties of Transition Systems」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル