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.
Year
DOI
Venue
2018
10.1109/APSEC.2018.00024
2018 25th Asia-Pacific Software Engineering Conference (APSEC)
Keywords
Field
DocType
Tools,Semantics,Mathematical model,Cognition,Metadata,Automation,Software engineering
Systems engineering,Computer science,Theoretical computer science,Invariant (mathematics)
Conference
ISSN
ISBN
Citations 
1530-1362
978-1-7281-1970-0
0
PageRank 
References 
Authors
0.34
0
3
Name
Order
Citations
PageRank
Daniel Găină1425.30
Ionut Tutu264.52
Adrián Riesco315724.66