Equational Abstraction Refinement for Certified Tree Regular Model CheckingReport as inadecuate

Equational Abstraction Refinement for Certified Tree Regular Model Checking - Download this document for free, or read online. Document in PDF available to download.

1 LIFO - Laboratoire d-Informatique Fondamentale d-Orléans 2 CELTIQUE - Software certification with semantic analysis Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL 3 S4 - System synthesis and supervision, scenarios IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique

Abstract : Tree Regular Model Checking TRMC is the name of a family of techniques for analyzing in nite-state systems in which states are represented by trees and sets of states by tree automata. The central problem is to decide whether a set of bad states belongs to the set of reachable states. An obstacle is that this set is in general neither regular nor computable in nite time. This paper proposes a new CounterExample Guided Abstraction Re- nement CEGAR algorithm for TRMC. Our approach relies on a new equational-abstraction based completion algorithm to compute a regular overapproximation of the set of reachable states in nite time. This set is represented by R=E-automata, a new extended tree automaton formalism whose structure can be exploited to detect and remove false positives in an e cient manner. Our approach has been implemented in TimbukCEGAR, a new toolset that is capable of analyzing Java programs by exploiting an elegant translation from the Java byte code to term rewriting systems. Experiments show that TimbukCEGAR outperforms existing CEGAR-based completion algorithms. Contrary to existing TRMC toolsets, the answers provided by TimbukCEGAR are certi- ed by Coq, which means that they are formally proved correct.

keyword : Model-checking tree automaton refinement

Author: Yohan Boichut - Benoît Boyer - Thomas Genet - Axel Legay -

Source: https://hal.archives-ouvertes.fr/


Related documents