Specification and Verification of Invariant Properties of Transition Systems

Daniel Gaina, Ionut Tutu, Adrian Riesco

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

1 Citation (Scopus)

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.

Original languageEnglish
Title of host publicationProceedings - 25th Asia-Pacific Software Engineering Conference, APSEC 2018
PublisherIEEE Computer Society
Pages99-108
Number of pages10
ISBN (Electronic)9781728119700
DOIs
Publication statusPublished - Jul 2 2018
Event25th Asia-Pacific Software Engineering Conference, APSEC 2018 - Nara, Japan
Duration: Dec 4 2018Dec 7 2018

Publication series

NameProceedings - Asia-Pacific Software Engineering Conference, APSEC
Volume2018-December
ISSN (Print)1530-1362

Conference

Conference25th Asia-Pacific Software Engineering Conference, APSEC 2018
CountryJapan
CityNara
Period12/4/1812/7/18

    Fingerprint

All Science Journal Classification (ASJC) codes

  • Software

Cite this

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