TY - GEN
T1 - Tableaux for verification of data-centric processes
AU - Bauer, Andreas
AU - Baumgartner, Peter
AU - Diller, Martin
AU - Norrish, Michael
PY - 2013
Y1 - 2013
N2 - Current approaches to analyzing dynamic systems are mostly grounded in propositional (temporal) logics. As a consequence, they often lack expressivity for modelling rich data structures and reasoning about them in the course of a computation. To address this problem, we propose a rich modelling framework based on first-order logic over background theories (arithmetics, lists, records, etc) and state transition systems over corresponding interpretations. On the reasoning side, we introduce a tableau calculus for bounded model checking of properties expressed in a certain fragment of CTL* over that first-order logic. We also describe a k-induction scheme on top of that calculus for proving safety properties, and we report on first experiments with a prototypical implementation.
AB - Current approaches to analyzing dynamic systems are mostly grounded in propositional (temporal) logics. As a consequence, they often lack expressivity for modelling rich data structures and reasoning about them in the course of a computation. To address this problem, we propose a rich modelling framework based on first-order logic over background theories (arithmetics, lists, records, etc) and state transition systems over corresponding interpretations. On the reasoning side, we introduce a tableau calculus for bounded model checking of properties expressed in a certain fragment of CTL* over that first-order logic. We also describe a k-induction scheme on top of that calculus for proving safety properties, and we report on first experiments with a prototypical implementation.
UR - http://www.scopus.com/inward/record.url?scp=84885722188&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-40537-2_5
DO - 10.1007/978-3-642-40537-2_5
M3 - Conference contribution
SN - 9783642405365
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 28
EP - 43
BT - Automated Reasoning with Analytic Tableaux and Related Methods - 22nd International Conference, TABLEAUX 2013, Proceedings
T2 - 22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2013
Y2 - 16 September 2013 through 19 September 2013
ER -