Skip to Main content Skip to Navigation
Theses

Model Checking and Theorem Proving

Abstract : Model checking is a technique for automatically verifying correctness properties of finite systems. Normally, model checking tools enjoy two remarkable features: they are fully automatic and a counterexample will be produced if the system fails to satisfy the property. Deduction Modulo is a reformulation of Predicate Logic where some axioms—possibly all—are replaced by rewrite rules. The focus of this dissertation is to give an encoding of temporal properties expressed in CTL as first-order formulas, by translating the logical equivalence between temporal operators into rewrite rules. This way, proof-search algorithms designed for Deduction Modulo, such as Resolution Modulo or Tableaux Modulo, can be used to verify temporal properties of finite transition systems. To achieve the aim of solving model checking problems with an off-the-shelf automated theorem prover, three works are included in this dissertation. First, we address the graph traversal problems in model checking with automated theorem provers. As a preparation work, we propose a way of encoding a graph as a formula such that the traversal of the graph corresponds to resolution steps. Then we present the way of translating model checking problems as proving first-order formulas in Deduction Modulo. The soundness and completeness of our method shows that solving CTL model checking problems with automated theorem provers is feasible. At last, based on the theoretical basis in the second work, we propose a symbolic model checking method. This method is implemented in iProver Modulo, which is a first-order theorem prover uses Polarized Resolution Modulo.
Document type :
Theses
Complete list of metadata

Cited literature [59 references]  Display  Hide  Download

https://hal.inria.fr/tel-01251073
Contributor : Kailiang Ji <>
Submitted on : Tuesday, January 19, 2016 - 6:03:00 PM
Last modification on : Saturday, March 28, 2020 - 2:20:13 AM
Long-term archiving on: : Thursday, November 10, 2016 - 9:14:16 PM

Identifiers

  • HAL Id : tel-01251073, version 1

Collections

Citation

Kailiang Ji. Model Checking and Theorem Proving. Computation and Language [cs.CL]. Paris Diderot, 2015. English. ⟨tel-01251073⟩

Share

Metrics

Record views

452

Files downloads

756