SMT-based verification analyzes reachability for transition systems represented by SMT formulae. Depending on the theories and the kinds of systems considered, various approaches have been proposed. Together, they form the Verification Modulo Theory (VMT) framework. This thesis delves into SMT-based verification of parameterized systems, emphasizing the challenges and novel solutions in verifying systems with an unbounded number of components. In this thesis, we first introduce a general framework to model such systems. Then, we introduce two novel algorithms that leverage the strengths of SMT for the verification of parameterized systems, focusing on the automation and reduction of computational complexity inherent in such tasks. These algorithms are designed to improve upon existing verification methods by offering enhanced scalability and automation, making them particularly suited for the analysis of distributed systems, network protocols, and concurrent programming models where traditional approaches may fail. Moreover, we introduce an algorithm for compositional verification that advances the capability to modularly verify complex systems by decomposing the verification task into smaller, more manageable sub-tasks. Additionally, we discuss the potential and ongoing application of these algorithms in an industrial project focusing on the design of interlocking logic. This particular application demonstrates the practical utility of our algorithms in a real-world setting, highlighting their effectiveness in improving the safety and reliability of critical infras- tructure. The theoretical advancements proposed in this thesis are complemented by a rig- orous experimental evaluation, demonstrating the applicability and effectiveness of our methods across a range of verification scenarios. Our work is implemented within an ex- tended framework of the MathSAT SMT solver, facilitating its integration into existing verification workflows. Overall, this research contributes to the theoretical underpinnings of Verification Modulo Theories (VMT) and offers tools and methodologies for the verification community, enhancing the capability to verify complex parameterized systems with greater efficiency and reliability.

Ce travail s'inscrit dans le cadre de la vérification formelle de programmes. La vérification de modèle permet de s'assurer qu'une propriété est vérifiée par le modèle du système. Cette thèse étudie la vérification paramétrée de réseaux composés d'un nombre non borné de processus identiques où le nombre de processus est considéré comme un paramètre. Concernant les réseaux de protocoles probabilistes temporisés nous montrons que les problèmes de l'accessibilité et de synchronisation sont indécidables pour des topologies de communication en cliques. Cependant, en considérant des pertes et créations probabiliste de processus ces problèmes deviennent décidables. Pour ce qui est des réseaux dans lequel les messages n'atteignent qu'une sous partie des composants choisie de manière non-déterministe, nous prouvons que le problème de l'accessibilité paramétrée est décidable grâce à une réduction à un nouveau modèle de jeux à deux joueurs distribué pour lequel nous montrons que l'on peut décider de l'existence d'une stratégie gagnante en coNP. Finalement, nous considérons des stratégies locales qui permettent d'assurer que les processus effectuent leurs choix non-déterministes uniquement par rapport a leur connaissance locale du système. Sous cette hypothèse de stratégies locales, nous prouvons que les problèmes de l'accessibilité et de synchronisation paramétrées sont NP-complet. / This thesis deals with formal verification of distributed systems. Model checking is a technique for verifying that the model of a system under study fulfills a given property. This PhD investigates the parameterized verification of networks composed of many identical processes for which the number of processes is the parameter. Considering networks of probabilistic timed protocols, we show that the parameterized reachability and synchronization problems are undecidable when the communication topology is a clique. However, assuming probabilistic creation and deletion of processes, the problems become decidable. Regarding selective networks, where the messages only reach a subset of the components, we show decidability of the parameterized reachability problem thanks to reduction to a new model of distributed two-player games for which we prove decidability in coNP of the game problem. Finally, we consider local strategies that enforce all processes to resolve the non-determinism only according to their own local knowledge. Under this assumption of local strategy, we were able to show that the parameterized reachability and synchronization problems are NP-complete.

<p> </p> <p>Distributed agreement-based systems use common distributed agreement protocols such as leader election and consensus as building blocks for their target functionality—processes in these systems may need to agree on a leader, on the members of a group, on owners of locks, or on updates to replicated data. Such distributed agreement-based systems are common and potentially permit modular, scalable verification approaches that mimic their modular design. Interestingly, while there are many verification efforts that target agreement protocols themselves, little attention has been given to distributed agreement-based systems that build on top of these protocols. </p> <p>In this work, we aim to develop a fully-automated, modular, and usable parameterized verification approach for distributed agreement-based systems. To do so, we need to overcome the following challenges. First, the fully automated parameterized verification problem, i.e, the problem of algorithmically checking if the system is correct for any number of processes, is a well-known <em>undecidable </em>problem. Second, to enable modular verification that leverages the inherently-modular nature of these agreement-based systems, we need to be able to support <em>abstractions </em>of agreement protocols. Such abstractions can replace the agreement protocols’ implementations when verifying the overall system; enabling modular reasoning. Finally, even when the verification is fully automated, a system designer still needs assistance in <em>modeling </em>their distributed agreement-based systems. </p> <p>We systematically tackle these challenges through the following contributions. </p> <p>First, we support efficient, decidable verification of distributed agreement-based systems by developing a computational model—the GSP model—for reasoning about distributed (agreement-based) systems that admits decidability and <em>cutoff </em>results. Cutoff results enable practical verification by reducing the parameterized verification problem to the verification problem of a system with a fixed, finite number of processes. The GSP model supports generalized communication primitives and global guards, both of which are essential to enable abstractions of agreement protocols. </p> <p>Then, we address the usability and modularity aspects by developing a framework, QuickSilver, tailored for modeling and modular parameterized verification of distributed agreement-based systems. QuickSilver provides an intuitive domain-specific language, called Mercury, that is equipped with two agreement primitives capable of abstracting away agreement protocols when modeling agreement-based systems; enabling modular verification. QuickSilver extends the decidability and cutoff results of the GSP model to provide fully automated, efficient parameterized verification for a large class of systems modeled in Mercury. </p> <p>Finally, we leverage synthesis techniques to further enhance the usability of our approach and propose Cinnabar, a tool that supports synthesis of distributed agreement-based systems with efficiently-decidable parameterized verification. Cinnabar allows a system de- signer to provide a sketch of their Mercury model and uses a counterexample-guided synthesis procedure to search for model completions that both belong to the efficiently-decidable fragment of Mercury and are correct. </p> <p>We evaluate our contributions on various interesting distributed agreement-based systems adapted from real-world applications, such as a data store, a lock service, a surveillance system, a pathfinding algorithm for mobile robots, and more. </p>

<p dir="ltr">Distributed protocols, with their immense state spaces and complex behaviors, have long been popular targets for formal verification. Cutoff reductions offer an enticing path for verifying parameterized distributed systems, composed of arbitrarily many processes. While parameterized verification (i.e., algorithmically checking correctness of a system with an arbitrary number of processes) is generally undecidable, these reductions allow one to verify certain classes of parameterized systems by reducing verification of an infinite family of systems to that of a single finite instance. The finiteness of the resulting target system enables fully-automated verification of the entire unbounded system family. In this work, we aim to establish pathways for automated verification via cutoff reductions which emphasize a modular approach to establishing correctness.</p><p dir="ltr">First, we consider distributed, agreement-based (DAB) systems. That is, systems which are built on top of agreement protocols, such as agreement and consensus. While much attention has been paid to the correctness of the protocols themselves, relatively little consideration as been given to systems which utilize these protocols to achieve some higher-level functionality. To this end, we present the GSP model, a system model based on two types of globally-synchronous transitions: k-sender and k-maximal, the latter of which was introduced by this author. This model enables us to formalize systems built on distributed consensus and leader election, and define conditions under which such systems may be verified automatically, despite the involvement of an arbitrary number of participant processes (a problem which is generally undecidable). Further, we identify conditions under which these systems can be verified efficiently and provide proofs of their correctness developed in part by this author. We then present QuickSilver, a user-friendly framework for designing and verifying parameterized DAB systems and, on this author’s suggestion, lift the GSP decidability results to QuickSilver using this author’s notion of when the behavior of all processes in the system can be separated into sections of their control flow, called “phase analysis”.</p><p dir="ltr">Next, we address verification of systems beyond agreement-based protocols. We find that, among parameterized systems, a class of systems we refer to as star-networked systems has received limited attention as the subject of cutoff reductions. These systems combine heterogeneous client and server process definitions with both pairwise and broadcast communication, so they often fall outside the requirements of existing cutoff computations. We address these challenges in a novel cutoff reduction based on careful analysis of the interactions between a central process and an arbitrary number of peripheral client processes as they progress toward an error state. The key to our approach rests on identifying systems in which the central process coordinates primarily with a finite number of core client processes, and outside of such core clients, the system’s progress can be enabled by a finite number of auxiliary clients.</p><p dir="ltr">Finally, we examine systems that are doubly-unbounded, in particular, parameterized DAB systems that additionally have unbounded data domains. We present a novel reduction which leverages value symmetry and a new notion of data saturation to reduce verification of doubly-unbounded DAB systems to model checking of small, finite-state systems. We also demonstrate that this domain reduction can be applied beyond DAB systems, including to star-networked systems.</p><p dir="ltr">We implement our reductions in several frameworks to enable efficient verification of sophisticated DAB and star-networked system models, including the arbitration mechanism for a consortium blockchain, a simple key-value store, and a lock server. We show that, by reducing the complexity of verification problems, cutoff reductions open up avenues for the application of a variety of verification techniques, including further reduction.</p>

No description available.