Tableaux for verification of data-centric processes

Andreas Bauer, Peter Baumgartner, Martin Diller, Michael Norrish

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    1 Citation (Scopus)

    Abstract

    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.

    Original languageEnglish
    Title of host publicationAutomated Reasoning with Analytic Tableaux and Related Methods - 22nd International Conference, TABLEAUX 2013, Proceedings
    Pages28-43
    Number of pages16
    DOIs
    Publication statusPublished - 2013
    Event22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2013 - Nancy, France
    Duration: 16 Sept 201319 Sept 2013

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume8123 LNAI
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2013
    Country/TerritoryFrance
    CityNancy
    Period16/09/1319/09/13

    Fingerprint

    Dive into the research topics of 'Tableaux for verification of data-centric processes'. Together they form a unique fingerprint.

    Cite this