Related papers: Complete Local Reasoning About Parameterized Progr…
In this paper we deal with verification of safety properties of parameterized systems with a tree topology. The verification problem is translated to a purely logical problem of finding a finite countermodel for a first-order formula, which…
A long-standing research problem in security protocol design is how to efficiently verify security protocols with tamper-resistant global states. In this paper, we address this problem by first proposing a protocol specification framework,…
Parameterized verification of coverability in broadcast networks with finite state processes has been studied for different types of models and topologies. In this paper, we attempt to develop a theory of broadcast networks in which the…
Inspired by distributed applications that use consensus or other agreement protocols for global coordination, we define a new computational model for parameterized systems that is based on a general global synchronization primitive and…
We address the problem of statically checking safety properties (such as assertions or deadlocks) for parameterized phaser programs. Phasers embody a non-trivial and modern synchronization construct used to orchestrate executions of…
Proving programs terminating is a fundamental computer science challenge. Recent research has produced powerful tools that can check a wide range of programs for termination. The analog for probabilistic programs, namely termination with…
Interlocking logics are at the core of critical systems controlling the traffic within stations. In this paper, we consider a generic interlocking logic, which can be instantiated to control a wide class of stations. We tackle the problem…
We consider concurrent systems consisting of a finite but unknown number of components, that are replicated instances of a given set of finite state automata. The components communicate by executing interactions which are simultaneous…
In this paper we investigate to which extent a very simple and natural "reachability as deducibility" approach, originated in the research in formal methods in security, is applicable to the automated verification of large classes of…
The integration of neural networks into safety-critical systems has shown great potential in recent years. However, the challenge of effectively verifying the safety of Neural Network Controlled Systems (NNCS) persists. This paper…
We present a method for the automated verification of temporal properties of infinite state systems. Our verification method is based on the specialization of constraint logic programs (CLP) and works in two phases: (1) in the first phase,…
We study verification problems for autonomous swarms of mobile robots that self-organize and cooperate to solve global objectives. In particular, we focus in this paper on the model proposed by Suzuki and Yamashita of anonymous robots…
Continuous-variable quantum states are of particular importance in various quantum information processing tasks including quantum communication and quantum sensing. However, a bottleneck has emerged with the fast increasing in size of the…
We study the implementability problem for an expressive class of symbolic communication protocols involving multiple participants. Our symbolic protocols describe infinite states and data values using dependent refinement predicates.…
Universal quantifiers occur frequently in proof obligations produced by program verifiers, for instance, to axiomatize uninterpreted functions and to express properties of arrays. SMT-based verifiers typically reason about them via…
The automatic verification of programs that maintain unbounded low-level data structures is a critical and open problem. Analyzers and verifiers developed in previous work can synthesize invariants that only describe data structures of…
We consider parameterized verification of systems executing according to the total store ordering (TSO) semantics. The processes manipulate abstract data types over potentially infinite domains. We present a framework that translates the…
In this paper we study possibilities of using hierarchical reasoning, symbol elimination and model generation for the verification of parametric systems, where the parameters can be constants or functions. Our goal is to automatically…
We present the first fully automatic framework for verifying relational properties of parameterized quantum programs, i.e., a program that, given an input size, generates a corresponding quantum circuit. We focus on verifying input-output…
We propose a new abstract formalism for probabilistic timed systems, Parametric Interval Probabilistic Timed Automata, based on an extension of Parametric Timed Automata and Interval Markov Chains. In this context, we consider the…