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ă | 1 | 42 | 5.30 |
Ionut Tutu | 2 | 6 | 4.52 |
Adrián Riesco | 3 | 157 | 24.66 |