Catálogo de publicaciones - libros

A Craig interpolant for a mutually inconsistent pair of formulas (,) is a formula that is (1) implied by , (2) inconsistent with , and (3) expressed over the common variables of and . An interpolant can be efficiently derived from a refutation of ∧ , for certain theories and proof systems. We will discuss a number of applications of this concept in finite- and infinite-state model checking.

We address the problem of automatic verification of programs with dynamic data structures. We consider the case of sequential, non-recursive programs manipulating 1-selector-linked structures such as traditional linked lists (possibly sharing their tails) and circular lists. We propose an automata-based approach for a symbolic verification of such programs using the regular model checking framework. Given a program, the configurations of the memory are systematically encoded as words over a suitable finite alphabet, potentially infinite sets of configurations are represented by finite-state automata, and statements of the program are automatically translated into finite-state transducers defining regular relations between configurations. Then, abstract regular model checking techniques are applied in order to automatically check safety properties concerning the shape of the computed configurations or relating the input and output configurations. For this particular purpose, we introduce new techniques for the computation of abstractions of the set of reachable configurations and to refine these abstractions if spurious counterexamples are detected. Finally, we present experimental results showing the applicability of the approach and its efficiency.

is the name of a family of techniques for analyzing infinite-state systems in which states are represented by words, sets of states by finite automata, and transitions by finite-state transducers. The central problem is to compute the transitive closure of a transducer. A main obstacle is that the set of reachable states is in general not regular. Recently, regular model checking has been extended to systems with tree-like architectures. In this paper, we provide a procedure, based on a new implementable acceleration technique, for computing the transitive closure of a tree transducer. The procedure consists of incrementally adding new transitions while merging states which are related according to a pre-defined equivalence relation. The equivalence is induced by a and an simulation relation which can be efficiently computed. Our technique can also be used to compute the set of reachable states without computing the transitive closure. We have implemented and applied our technique to several protocols.

A novel machine learning based approach was proposed recently as a complementary technique to the acceleration based methods for verifying infinite state systems. In this method, the set of states satisfying a fixpoint property is learnt as opposed to being iteratively computed. We extend the machine learning based approach to verifying general -regular properties that include both safety and liveness. To achieve this, we first develop a new fixpoint based characterization for the verification of -regular properties. Using this characterization, we present a general framework for verifying infinite state systems. We then instantiate our approach to the context of regular model checking where states are represented as strings over a finite alphabet and the transition relation of the system is given as a finite state transducer; unlike previous learning based algorithms, we make no assumption about the transducer being length-preserving. Using Angluin’s L* algorithm for learning regular languages, we develop an algorithm for verification of -regular properties of such infinite state systems. The algorithm is a complete verification procedure for systems for whom the fixpoint can be represented as a regular set. We have implemented the technique in a tool called and use it to analyze some examples.

Searching the state space of a system using enumerative and on-the-fly depth-first traversal is an established technique for model checking finite-state systems. In this paper, we propose algorithms for on-the-fly exploration of recursive state machines, or equivalently pushdown systems, which are suited for modeling the behavior of procedural programs. We present algorithms for reachability (is a bad state reachable?) as well as for fair cycle detection (is there a reachable cycle with progress?). We also report on an implementation of these algorithms to check safety and liveness properties of recursive boolean programs, and its performance on existing benchmarks.

(WSTS) are a broad and well-studied class of infinite-state systems, for which the problem of verifying the reachability of an upward-closed set of error states is decidable (subject to some technicalities). Recently, Bingham proposed a new algorithm for this problem, but applicable only to the special cases of broadcast protocols and petri nets. The algorithm exploits finite-state symbolic model checking and was shown to outperform the classical WSTS verification algorithm on a contrived example family of petri nets.

In this work, we generalize the earlier results to handle a larger class of WSTS, which we dub , that includes broadcast protocols, petri nets, context-free grammars, and lossy channel systems. We also add an optimization to the algorithm that accelerates convergence. In addition, we introduce a new reduction that soundly converts the verification of parameterized systems with unbounded conjunctive guards into a verification problem on nicely sliceable WSTS. The reduction is complete if a certain decidable side condition holds. This allows us to access industrially relevant challenge problems from parameterized memory system verification. Our empirical results show that, although our new method performs worse than the classical approach on small petri net examples, it performs substantially better on the larger examples based on real, parameterized protocols (e.g., German’s cache coherence protocol, with data paths).

The interaction among concurrently executing threads of a program results in insidious programming errors that are difficult to reproduce and fix. Unfortunately, the problem of verifying a concurrent boolean program is undecidable [24]. In this paper, we prove that the problem is decidable, even in the presence of unbounded parallelism, if the analysis is restricted to executions in which the number of context switches is bounded by an arbitrary constant. Restricting the analysis to executions with a bounded number of context switches is unsound. However, the analysis can still discover intricate bugs and is sound up to the bound since within each context, a thread is fully explored for unbounded stack depth. We present an analysis of a real concurrent system by the ZING model checker which demonstrates that the ability to model check with arbitrary but fixed context bound in the presence of unbounded parallelism is valuable in practice. Implementing context-bounded model checking in ZING is left for future work.

We describe a new tool called -Prover which is an interactive theorem prover dedicated to refinement proofs within the process algebra . It aims specifically at proofs for infinite state systems, which may also involve infinite non-determinism. Semantically, -Prover supports both the theory of complete metric spaces as well as the theory of complete partial orders. Both these theories are implemented for infinite product spaces. Technically, -Prover is based on the theorem prover Isabelle. It provides a deep encoding of . The tool’s architecture follows a generic approach which makes it easy to adapt it for various models besides those studied here: the stable failures model and the traces model .

Fair discrete systems (FDSs) are a computational model of concurrent programs where fairness assumptions are specified in terms of sets of states. The analysis of fair discrete systems involves a non-trivial interplay between fairness and well-foundedness (ranking functions). This interplay has been an obstacle for automation. The contribution of this paper is a new analysis of temporal properties of FDSs. The analysis uses a domain of binary relations over states labeled by sets of indices of fairness requirements. The use of labeled relations separates the reasoning on well-foundedness and fairness.

The Paige and Tarjan algorithm (PT) for computing the coarsest refinement of a state partition which is a bisimulation on some Kripke structure is well known. It is also well known in abstract model checking that bisimulation is equivalent to strong preservation of CTL and in particular of Hennessy-Milner logic. Building on these facts, we analyze the basic steps of the PT algorithm from an abstract interpretation perspective, which allows us to reason on strong preservation in the context of generic inductively defined (temporal) languages and of abstract models specified by abstract interpretation. This leads us to design a generalized Paige-Tarjan algorithm, called GPT, for computing the minimal refinement of an abstract interpretation-based model that strongly preserves some given language. It turns out that PT can be obtained by instantiating GPT to the domain of state partitions for the case of strong preservation of Hennessy-Milner logic. We provide a number of examples showing that GPT is of general use. We show how two well-known efficient algorithms for computing simulation and stuttering equivalence can be viewed as simple instances of GPT. Moreover, we instantiate GPT in order to design a (||||)-time algorithm for computing the coarsest refinement of a given partition that strongly preserves the language generated by the reachability operator .