PV 2014
The First Workshop on Parameterized Verification
A Satellite Event of Concur 2014
Rome, September 6, 2014


Goal | Organizers | Program | Registration | Concur Home Page

Goal

Systems composed of a finite but possibly arbitrary number of identical components occur everywhere from hardware design (e.g. cache coherence protocols) to distributed applications (e.g. client-server applications). Parameterized verification is the task of verifying the correctness of this kind of systems regardless the number of their components. The workshop is aimed at bringing together researchers working on Parameterized Verification using

Organizing Committee


Preliminary Program


Time Schedule (PDF)
List of abstracts
Philippe Schnoebelen (LSV Cachan):
Well-Structured Parameterized Networks of Systems

Abstract:
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


Lenore Zuck (UIC)
Verification of Parameterized Systems: Theory and Practice

Abstract:
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.

Andreas Podelski (Univ. Freiburg)
Proof Spaces for Unbounded Parallelism

Abstract:
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.
Barbara Koenig (Univ. Duisburg-Essen):
Decidability Results for Graph Transformation Systems

Abstract:
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

Pierre Ganty (IMDEA Software Institute)
Parameterized Verification of Asynchronous Shared-Memory Systems

Abstract:
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)
Roland Meyer (Univ. Kaiserslautern)
Dimensions of Mobility

Abstract:
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.
Silvio Ranise (FBK, Trento):
Parameterized Verification goes Safety Analysis of Access Control Policies

Abstract:
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).
Marco Montali (Free University of Bozen-Bolzano):
Verification of Parameterized, Data-Aware Dynamic Systems

Abstract:

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)
Jacopo Mauro (Univ. Bologna):
Complexity Bounds for Software Component Reconfiguration

Abstract:
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)
Josef Widder (TUV)
Fault-Tolerant Distributed Algorithms: Modeling and Parametrized Model Checking

Abstract:
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
Jan Stuckrath (Univ. Duisburg-Essen):
Parameterized Verification of Graph Transformation Systems with Whole Neighbourhood Operations

Abstract:
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)
Francesco Spegni (UnivPM):
Parameterized Model Checking of Rendezvous Systems

Abstract:
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.
Lukas Holik (Brno Univ. of Technology):
Parameterized Verification through View Abstraction

Abstract:
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)
Panagiotis Kouvarous (Imperial College):
Cutoff Techniques in Verification of Open Multi-Agent Systems

Abstract:
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)
Maurizio Proietti (IASI-CNR, Rome)
Verification of Array Manipulating Programs: A Transformational Approach

Abstract:
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

Venue and Registration


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 July 27