Abstract The TLA $$^+$$ + language has been widely used, both in academia and industry, to specify and reason about distributed systems. This paper presents Apalache , an efficient and flexible symbolic model checker for TLA $$^+$$ + . Apalache ’s engine is based on bounded model checking, with symbolic transitions being extracted from TLA $$^+$$ + specifications and verification conditions suitable for satisfiability modulo theories (SMT) solvers being generated from them. Reasoning can be done in terms of safety and liveness properties, with liveness checking realised via a liveness-to-safety reduction. Apalache ’s flexibility lies in its three complementary functionalities: bounded exhaustive verification, for bounded guarantees, randomised symbolic execution, for prototyping and bug detection, and inductiveness checking, for unbounded guarantees. The paper describes Apalache ’s architecture and features, including its support for PlusCal and Quint, two languages that share the same semantic foundation as TLA $$^+$$ + . Industrial usage of Apalache is also presented, together with a case study which illustrates how Apalache can be used to verify the agreement property of a consensus protocol.

Abstract Parameterized programs are composed of an arbitrary number of concurrent, infinite-state threads. Automated safety and liveness proofs of such parameterized software are hard; state-of-the-art methods for their formal verification rely on intricate abstractions and complicated proof techniques that impede automation. In this paper, we introduce thread-modular counter abstraction (TMCA), a lean new abstraction technique to replace the existing heavy proof machinery. TMCA is a structured abstraction framework built from a novel combination of counter abstraction, thread-modular reasoning, and predicate abstraction. Its major strength lies in reducing the parameterized verification problem to the sequential setting, for which powerful proof procedures, efficient heuristics, and effective automated tools have been developed over the past decades. In this work, we first introduce the TMCA abstraction paradigm, then present a fully automated method for parameterized safety proofs, and finally discuss its application to automated termination and liveness proofs of parameterized software.

Abstract We present a thread-modular proof method for complexity and resource bound analysis of concurrent, shared-memory programs. To this end, we lift Jones’ rely-guarantee reasoning to assumptions and commitments capable of expressing bounds. The compositionality (thread-modularity) of this framework allows us to reason about parameterized programs, i.e., programs that execute arbitrarily many concurrent threads. We automate reasoning in our logic by reducing bound analysis of concurrent programs to the sequential case. As an application, we automatically infer time complexity for a family of fine-grained concurrent algorithms, lock-free data structures, to our knowledge for the first time.

Automated safety proofs of parameterized software are hard: State-of-the-art methods rely on intricate abstractions and complicated proof techniques that often impede automation.We replace this heavy machinery with a clean abstraction framework built from a novel combination of counter abstraction, thread-modular reasoning, and predicate abstraction.Our fully automated method proves parameterized safety for a wide range of classically challenging examples in a straight-forward manner.

We present a thread-modular proof method for complexity and resource bound analysis of concurrent, shared-memory programs, lifting Jones' rely-guarantee reasoning to assumptions and commitments capable of expressing bounds. We automate reasoning in this logic by reducing bound analysis of concurrent programs to the sequential case. Our work is motivated by its application to lock-free data structures, fine-grained concurrent algorithms whose time complexity has to our knowledge not been inferred automatically before.

We study empirical metrics for software source code, which can predict the performance of verification tools on specific types of software. Our metrics comprise variable usage patterns, loop patterns, as well as indicators of control-flow complexity and are extracted by simple data-flow analyses. We demonstrate that our metrics are powerful enough to devise a machine-learning based portfolio solver for software verification. We show that this portfolio solver would be the (hypothetical) overall winner of the international competition on software verification (SV-COMP) in three consecutive years (2014-2016). This gives strong empirical evidence for the predictive power of our metrics and demonstrates the viability of portfolio solvers for software verification. Moreover, we demonstrate the flexibility of our algorithm for portfolio construction in novel settings: originally conceived for SV-COMP'14, the construction works just as well for SV-COMP'15 (considerably more verification tasks) and for SV-COMP'16 (considerably more candidate verification tools).