| ||||
| ||||
Abstract: A program is data independent in a type variable X approximately when it makes sense for any non-empty instantiation of X. It is frequently possible to prove by a finite amount of model checking that data independent programs satisfy a specification independently of this type, for example by calculating a threshold (size of type beyond which the result cannot vary). The basic theory does not, however, encompass parallel compositions indexed over X. Neither do conventional inductive techniques when the component processes are themselves parameterised by X (i.e., they know the identities of the other nodes). It proves possible, however, to mix data independence (crucially using constant and predicate symbols) and induction to prove properties of such systems.
Abstract: We present a graph-theoretic statement of our implementation relations which relate the behaviour of implementation and specification systems built of communicating processes in the event that respective implementation and specification processes have differing interfaces. From these graph-theoretic statements we derive algorithms for the automatic verification of the implementation relations.
Full Paper: Postscript (gzipped)
Abstract: I give a brief account of a framework for infinite state model-checking developed at Edinburgh a few years ago, which provides a convenient way to include the use of constraint-solving methods in computer-aided model-checking.
Full Paper: Postscript (gzipped)
Abstract: Model checking temporal logic over abstracted transition systems under fairness constraints needs to be done with some care. This paper discusses why and how.
Full Paper: Postscript (gzipped)
Abstract: to be announced
Abstract: In this report, we show how to model a Petri net as a CLP program and how to solve some reachability problems in CLP using the fixed-point semantics of that program. We highlight the structural properties of both the logic part of the rules and the linear part of the constraint systems, which allow us to: ¥ traverse the state-space rather efficiently ¥ treat integer variables as real-valued ones, while retaining completeness of solving. We decompose the verification problem into two steps: first, we compute the set of all reachable states ; second, we check whether a given state property holds (or can be refuted) on that set. We finally report on our experiments with Prolog III.
Full Paper: PDF
Abstract: In our paper, we propose an efficient, optimized and totally automated technique used to perform an on-the-fly model checking of temporal properties exploiting symmetries. We use the symbolic approach associated with Well-formed Petri nets in order to drive the aggregation of either equivalent states and actions by the verification process. Hence, we alleviate and improve the exploitation of the system symmetries, which until now remained under the scope of computing a group of symmetries. From a practical point of view, we are now able to end the procedure as soon as a counter example is found and to show it into a symbolic form.
Full Paper: Postscript (gzipped)
Abstract: We introduce a lean and intuitive operational semantics of a characteristic subset of Standard Prolog (the whole logic and control, database updates and solution collecting). The Prolog computation is modelled as conditional rewriting of derivation states. Due to a novel linear representation of the Prolog tree traversal, our approach is especially suitable for modelling the control flow. The semantics is fully operational and implemented in Prolog. Some highlights of the approach: - a novel linear representation of the Prolog tree traversal, giving small and readable specifications - closer to the spirit of logic programming: by treating if-then-else and disjunction simply and compatibly with cut, by building the Prolog tree incrementally as a partial data structure, by treating findall and database updates without "external mechanisms" - a derivation is represented at the level of unification and backtracking - easy finding of ancestors, thus very suitable for defining cut and catch/throw in essentially the same user-friendly way
Full Paper: Postscript (gzipped)
Abstract: We consider prescriptive type systems for logic programs. In such systems, the typing is static, but it guarantees an operational property: if a program is well-typed, then all derivations starting in a well-typed goal are again well-typed. We show that this property is actually also declarative. This declarative view leads us to questioning the head condition. We provide a more general condition, thus reestablishing a certain symmetry between heads and body atoms. The condition ensures that in a derivation, only terms of identical type are unified. We discuss possible implications of this result.
Full Paper: Postscript (gzipped)
Abstract: not yet available
Abstract: For general broadcast protocols, the natural generalization of the Karp and Miller procedure does not terminate; even the problem of deciding if a broadcast protocol may exhibit infinite behaviour is undecidable. We define a subclass of broadcast protocols, called entropic broadcast protocols, which contains the MESI protocol, and we prove that the Generalized Karp and Miller procedure terminates and it gives a finite covering tree. We also prove that liveness is undecidable.
Full Paper: Postscript (gzipped)
Abstract: Weakly continuation-closed abstractions are known to preserve properties satisfied up to liveness, i.e. linear-time temporal properties under an abstract notion of fairness. Being defined on the complete behaviour of a concurrent system, weakly continuation-closed abstractions require, in principle, an exhaustive state-space construction prior to abstraction. Constructing the state-space of a practically relevant specification exhaustively, however, is usually unfeasible. Based on the notion of traces, i.e. certain equivalence classes of behaviours, we define trace reductions. We show that a trace reduction can be used on behalf of the complete behaviour of a concurrent system in order to compute abstractions as well as to check whether the abstractions are weakly continuation-closed. So trace reductions allow us to overcome the requirement of an exhaustive state-space construction prior to abstraction.
Full Paper: Postscript (gzipped)
Abstract: We present evidence that the refinement-based approach to verification does not seem to be very well suited for verifying temporal properties of a system. We then show how to (and how not to) perform LTL model checking of CSP processes using refinement checking in general and the FDR tool in particular. We show how one can handle (potentially) deadlocking systems, discuss the validity of our approach for infinite state systems, and shed light on the relationship between ``classical'' model checking and refinement checking.
Full Paper: Postscript (gzipped)