Loading...
Please wait, while we are loading the content...
Equational abstraction refinement for certified tree regular model checking (2012).
| Content Provider | CiteSeerX |
|---|---|
| Author | Boichut, Y. Boyer, B. Genet, T. Legay, A. |
| Abstract | Abstract. Tree Regular Model Checking (TRMC) is the name of a family of techniques for analyzing infinite-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 finite time. This paper proposes a new CounterExample Guided Abstraction Refinement (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 finite 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 efficient 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 certified by Coq, which means that they are formally proved correct. 1 |
| File Format | |
| Publisher Date | 2012-01-01 |
| Access Restriction | Open |
| Subject Keyword | Certified Tree Regular Model Checking Equational Abstraction Refinement Finite Time Reachable State Cegar-based Completion Algorithm Elegant Translation Java Byte Code New Toolset Completion Algorithm Trmc Toolsets Central Problem Efficient Manner Regular Overapproximation New Counterexample Guided Abstraction Refinement False Positive Approach Relies New Equational-abstraction New Extended Tree Automaton Formalism Tree Automaton Infinite-state System Java Program Tree Regular Model Checking Bad State Belongs |
| Content Type | Text |
| Resource Type | Article |
