TY - GEN
T1 - Specification and Verification of Invariant Properties of Transition Systems
AU - Gaina, Daniel
AU - Tutu, Ionut
AU - Riesco, Adrian
N1 - Publisher Copyright:
© 2018 IEEE.
PY - 2018/7/2
Y1 - 2018/7/2
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
T2 - 25th Asia-Pacific Software Engineering Conference, APSEC 2018
Y2 - 4 December 2018 through 7 December 2018
ER -