The First Workshop on Parameterized Verification

A Satellite Event of Concur 2014

Rome, September 6, 2014

- Automata and Logic, Term and Graph Rewriting, Petri nets, and Process Algebra and other specification languages,
- Validation methods like Assertional and Regular Model Checking, Reachability and Coverability Decision Procedures, Abstractions, Theorem Proving, Constraint Solvers.
- Applications to hardware design, cache coherence protocols, security and communication protocols, multithreaded and concurrent programs, programs with relaxed memory models, mobile and distributed systems, database languages and systems, biological systems.

- Parosh Abdulla, Uppsala University, Sweden (chair)
- Ahmed Bouajjani, Liafa, France
- Giorgio Delzanno, University of Genova, Italy (chair)
- Javier Esparza, TUM, Germany
- Alain Finkel, LSV-Cachan, France
- Barbara Koenig, Duisburg-Essen, Germany
- Rupak Majumdar, MPI-SWS, Germany
- Richard Mayr, Edinburgh, UK
- Kedar Namjoshi, Bell Labs, USA
- Andreas Podelski, Univ. Freiburg, Germany
- Philippe Schnoebelen, LSV-Cachan, France

Time Schedule (PDF)

Well-structured systems are a family of infinite-state models that support generic decidability results based on wqo theory. Among other applications, they are well suited to the modeling and the verification of parameterized networks of concurrent systems. In this talk, we survey a few instances of such well-structured parameterized networks and we describe recent results that shed new lights on the complexity and computing power of these models.

Slides in PDF

An introduction to the invisible invariants method for parameterized verification (based on deductive verification, model checking and theorem proving) and examples of its application to practical case-studies.

We present a proof system which can be used to exploit sequential verification technology for proving the correctness of multi-threaded programs with unboundedly many threads. The corresponding verification method can leverage the techniques of well-structured transition systems. The proof system is complete relative to more traditional proof systems for multi-threaded programs which allow features like thread quantification and control predicates.

Joint work with Azadeh Farzan and Zachary Kincaid.

Graph transformation systems are a natural modelling formalism for concurrent and distributed systems. In this talk I will give a tutorial-like introduction to graph transformation and then focus on decidability results for reachability and coverability problems. For a fixed initial configuration, we consider reachability of an entirely specified configuration and of a configuration that satisfies a given pattern (coverability). The former is a fundamental problem for any computational model, the latter is strictly related to verification of safety properties in which the pattern specifies an infinite set of bad configurations. We reformulate results obtained, e.g., for context-free graph grammars and concurrency models, such as Petri nets, in the more general setting of graph transformation systems and study new results for classes of models obtained by adding constraints on the form of reduction rules.

Slides in PDF

In this talk, we study the safety verification problem for parameterized systems consisting of a leader process and arbitrarily many anonymous and identical contributors. Processes communicate through a shared, bounded-value register. While each operation on the register is atomic, there is no synchronization primitive to execute a sequence of operations atomically. We analyze the complexity of the safety verification problem when processes are modeled by finite-state machines, pushdown machines, and Turing machines. Our proofs use a mix of combinatorial properties of the model and some language-theoretic constructions of independent interest.

Joint work with Javier Esparza (TUM) and Rupak Majumdar (MPI-SWS)

Mobile systems are characterized by a dynamic interconnection topology, which means components enter the system at runtime, build up links with others, and later vanish. General mobile systems are Turing complete which renders most verification problems undecidable. When looking for semantic restrictions, one is confronted with a trade-off between expressiveness of the resulting class of models and complexity of the associated algorithmic analysis. Over the past years, we have studied restrictions on natural and orthogonal dimensions in the behaviour of mobile applications. Degree-bounded systems limit the degree of parallelism, name-bounded systems limit the number of dynamic links, breadth-bounded systems restrict the number of components that connect to a link, and depth-bounded applications have a bounded number of layers. In this talk, we recall these classes and survey the results on their algorithmic analysis. From a modelling point of view, the classes form a hierarchy where degree-bounded systems at the bottom may be compared with Boolean programs and depth-bounded systems at the top generalize transfer Petri nets. From an algorithmic point of view, this increased expressiveness is reflected by a jump in the complexity from polynomial space to non-primitive recursive and undecidable, depending on the verification problem. So today we have a better understanding of how to model mobile applications and of what makes their analysis hard.

Access control is one of the most important mechanisms to ensure crucial security properties such as confidentiality, integrity, and availability in modern networked systems and applications. The complexity of today systems requires to express and enforce authorization that might depend on a variety of contextual information, e.g., the current time, the position of the users, selected parts of the system state, and even the history of the computations. Several models, languages, and enforcement mechanisms have been proposed for different scenarios. Unfortunately, this complicates the verification of safety, i.e. no permission is leaked to unauthorized users. To avoid these problems, we present an intermediate language called Action Language for Policy Specification (ALPS). Two desiderata drive its definition: (i) it should support as many models and policies as possible and (ii) it should be easily integrated in existing verification systems so that robust techniques (e.g., model checking or satisfiability solving) can be exploited to safety. We argue (i) by means of some examples and (ii) by showing how ALPS can be automatically translated to available verification techniques. In particular, we demonstrate how safety analysis can be made parametric in the number of users by a reduction to the reachability problem of symbolic transition systems that use formulae of Effectively Propositional Logic to represent sets of backward reachable states. We discuss the key ideas for the mechanization of the procedure where fix-point checks are reduced to SMT problems. Finally, we present how these ideas are applied to solve safety analysis problems for an important class of policies using the Role Based Access Control model, which is one of the more widely used in real-world systems.

Slides in PDF

Joint work with Riccardo Traverso (FBK, Trento) and Anh Truong (UniTn & FBK, Trento).

Dynamic systems that are parametric with respect to the manipulated data items have lately received increasing attention in the data and knowledge management communities. In general, these systems are able to inject and evolve unboundedly many data. Hence, their execution semantics is captured by means of transition systems with an infinite number of states. Notably, interesting decidability results have been recently produced for the formal verification of such systems under the hypothesis of state boundedness, which requires the existence of an overall bound on the amount of data stored in each single state along the system evolution. In this talk, we will introduce one of the most recent frameworks in this area, namely data-centric dynamic systems (DCDSs). We will then show that DCDSs are versatile enough to support parameterization w.r.t. different dimensions, such as business artifacts in data-aware business processes, names in extensions of Petri nets, as well as message correlations and number of interacting components in multi-agent systems. We will finally introduce preliminary results that rely on these correspondences. These results lay the ground for new insights in the verification of parameterized systems, paving the way towards novel forms of cross-fertilization between the area of data and knowledge management, and the area of formal methods.

Slides in PDF

Joint work with Diego Calvanese and Andrey Rivkin (Free University of Bozen-Bolzano)

In modern tools for automatic deployment and reconfiguration of applications, software components are usually modeled as grey-boxes that show (besides the typical provide and require interfaces) internal states that are relevant from a configuration management viewpoint. During the system reconfiguration phase, state transitions (corresponding to actions like "install", "configure", "run", "stop") can be executed only if all the provide and require dependencies are satisfied. The reconfiguration problem consists of checking whether, starting from an initial configuration, it is possible to reach a target component in a given internal state assuming to have an arbitrary amount of new components at our disposal. If there are conflicts between components we prove, relying on the theory of well-structured transition systems and well-known complexity results of Petri Nets, that the reconfiguration problem is decidable but Ackermann hard. If there are no conflicts, it turns out to be PSpace-hard.

Slides in PDF

Joint work with Gianluigi Zavattaro (Univ. Bologna)

Fault-tolerant distributed algorithms are naturally parametrized in the number of processes n and the assumed upper bound on the number of faulty processes t. Classic results in distributed computing theory show that correctness of certain algorithms can only be guaranteed under specific resilience conditions such as n > 3t. Moreover, the code typically refers to the parameters n and t. Unlike the classic parametrized model checking problem that deals with systems, parametrized only in the number of processes n, we are facing an interesting extension of the problem with multiple parameters, constraints on the parameters, and parametrized code. We present our recent results on modeling of fault-tolerant algorithms under asynchronous interleavings, unbounded but finite message delays, and different fault models, e.g., Byzantine and crash faults. Further, we present abstraction techniques that allow us to do parametrized model checking of safety and liveness for these kinds of algorithms. Besides, we will discuss many challenges in this area, yet to be addressed by the model checking community; for instance, the huge variety of computational models that differ in the restrictions on the interleavings, assumptions on message delays, and types of faults.

Slides in PDF

Joint work with Annu Gmeiner, Igor Konnov, Ulrich Schmid, and Helmut Veith

We introduce a new class of graph transformation systems in which rewrite rules can be guarded by universally quantified conditions on the neighbourhood of nodes. These conditions are defined via special graph patterns which may be transformed by the rule as well. For the new class for graph rewrite rules, we provide a symbolic procedure working on minimal representations of upward closed sets of configurations. We prove correctness and effectiveness of the procedure by a categorical presentation of rewrite rules as well as the involved order, and using results for well-structured transition systems. We apply the resulting procedure to the analysis of the Distributed Dining Philosophers protocol on an arbitrary network structure.

Slides in PDF

Joint work with Giorgio Delzanno (University of Genova)

A standard technique for solving the parameterized model checking problem is to reduce it to the classic model checking problem of finitely many finite-state systems. This work considers some of the theoretical power and limitations of this technique. We focus on concurrent systems in which processes communicate via pairwise rendezvous, as well as the special cases of disjunctive guards and token passing; specifications are expressed in indexed temporal logic without the next operator; and the underlying network topologies are generated by suitable Monadic Second Order Logic formulas and graph operations. First, we settle the exact computational complexity of the parameterized model checking problem for some of our concurrent systems, and establish new decidability results for others. Second, we consider the cases that model checking the parameterized system can be reduced to model checking some fixed number of processes, the number is known as a cutoff. We provide many cases for when such cutoffs can be computed, establish lower bounds on the size of such cutoffs, and identify cases where no cutoff exists. Third, we consider cases for which the parameterized system is equivalent to a single finite-state system (more precisely a Buechi word automaton), and establish tight bounds on the sizes of such automata.

Joint work with Benjamin Aminof, Tomer Kotek, Sasha Rubin, and Helmut Veith.

View abstraction is a simple and generic framework for verification of parameterized systems. The idea of the abstraction is to look at a system through a window of a limited size, where the size of the window determines the precision of the abstraction. The framework was shown to be complete for WSTS. Thanks to its simplicity, the framework is widely applicable to systems with many kinds of topologies and types of communication. Its expressiveness can be also extended to verify certain systems which are not WSTS and do not have good downward closed invariants, such as a full version of Szymanski's protocol.

Joint work with P. A. Abdulla and F. Haziza (Uppsala University)

While considerable progress has been made in the area of verification of multi-agent systems, most model checking techniques currently in use do not support open multi-agent systems where the number of components is unbounded. We put forward cutoff techniques for determining the number of agents that is sufficient to consider when checking temporal-epistemic specifications on a system of any size. We identify two special classes of interleaved interpreted systems for which we give a parameterised semantics and an abstraction methodology. We present an implementation on top of the open-source model checker MCMAS.

Slides in PDF

Joint work with A. Lomuscio (Imperial College)

We present a method for verifying properties of imperative programs that manipulate integer arrays of parameterized length. Imperative programs and their properties are represented by using Constraint Logic Programs (CLP) over integer arrays. Given a Hoare triple {Pre}Prog{Post} defining a partial correctness property of an imperative program Prog, we encode the negation of the property as a predicate Incorrect defined by a CLP program P, and we show that the property holds by proving that Incorrect is not a consequence of P. Program verification is performed by applying a sequence of semantics preserving transformation rules and deriving a new CLP program T such that Incorrect is a consequence of P iff it is a consequence of T. The rules are applied according to an automatic strategy whose objective is to derive a program T that satisfies one of the following properties: either (i) T is the empty set of clauses, hence proving that Incorrect does not hold and Prog is correct, or (ii) T contains the fact Incorrect, hence proving that Prog is incorrect. Our transformation strategy makes use of an axiomatization of the theory of arrays for manipulating array constraints, and also applies suitable combinations of widening and convex hull operators for generalizing linear integer constraints. The strategy has been implemented in the VeriMAP transformation system and it has been shown to be quite effective and efficient on a set of benchmark array programs taken from the literature.

Joint work with E. De Angelis, F. Fioravanti, and A. Pettorossi

PV 2014 will take place in The Faculty of Civil and Industrial Engineering of the Sapienza University of Rome

Registration fees are available in the Concur home page: Registration fees

The early registration deadline is