ABSTRACT. This tool paper presents CPA-Daemon, a microservice for continuous software verification of C code. CPA-Daemon provides full access to the verifier CPAchecker but adds a clear network interface based on gRPC and three different modes of operation: (1) running CPAchecker in a separate JVM, (2) running CPAchecker as a native executable compiled with GraalVM, and (3) running CPAchecker in a shared, continuously-running JVM. These novel execution modes greatly improve the response time of verification in different verification scenarios and enable the seamless integration of CPAchecker as a verification engine in other verification tooling. Our comparative evaluation shows that CPA-Daemon reduces the response time on small verification tasks down to 17 %, and that it can reduce the response time of existing cooperative verification techniques down to 70 %. While our implementation focuses on CPAchecker, the conceptual ideas are of general nature and can serve as a solution for other verification tools that face similar JVM-specific issues. CPA-Daemon is open source and will participate in artifact evaluation. It is available from https://gitlab.com/sosy-lab/software/cpa-daemon.

ABSTRACT. This work proposes a novel approach for automatic verification and synthesis of infinite-state reactive programs with respect to $CTL^*$ specifications, based on translation to Existential Horn Clauses (EHCs).

$CTL^*$ is a powerful temporal logic, which subsumes the temporal logics LTL and CTL, both widely used in specification, verification, and synthesis of complex systems.

EHCs with its solver E-HSF, is an extension of Constrained Horn Clauses, which includes existential quantification as well as the power of handling well-foundedness.

We develop the translation system Trans, which given a verification problem consisting of a program $P$ and a specification $\phi$, builds a set of EHCs which is satisfiable iff $P$ satisfies $\phi$. We also develop a synthesis algorithm that given a program with holes in conditions and assignments, fills the holes so that the synthesized program satisfies the given $CTL^*$ specification.

We prove that our verification and synthesis algorithms are both sound and relative complete. Finally, we present case studies to demonstrate the applicability of our algorithms for $CTL^*$ verification and synthesis.

ABSTRACT. Hyperproperties are system properties that relate multiple execution traces and, e.g., occur when specifying security and information-flow properties. Checking if a hyperproperty is satisfiable has many important applications, such as testing if some security property is contradictory, or analyzing implications and equivalences between information-flow policies. In this paper, we present HyperSAT, a tool that can automatically check satisfiability of hyperproperties specified in the temporal logic HyperLTL. HyperSAT reduces the problem to an equisatisfiable first-order logic (FOL) sentence, which allows us to leverage powerful FOL solvers. As such, HyperSAT is applicable to many formulas beyond the decidable $\exists^*\forall^*$ fragment of HyperLTL. Our experiments show that HyperSAT is particularly useful for proving that a formula is unsatisfiable, and complements existing bounded approaches to satisfiability.

ABSTRACT. Abstract. First-order logic has been established as an important tool for modeling and verifying intricate systems such as distributed protocols and concurrent systems. These systems are parametric in the number of nodes in the network or the number of threads, which is finite in any system instance, but unbounded. One disadvantage of first-order logic is that it cannot distinguish between finite and infinite structures, leading to spurious counter-examples. To mitigate this, we offer a verification approach that captures only finite system instances. Our approach is an adaptation of the cutoff method to systems modeled in first-order logic. The idea is to show that any safety violation in a system instance of size larger than some bound can be simulated by a safety violation in a system of a smaller size. The simulation provides an inductive argument for correctness in finite instances, reducing the problem to showing safety of instances with bounded size. To this end, we develop a framework to (i) encode such simulation relations in first-order logic and to (ii) validate the simulation relation by a set of verification conditions given to an SMT-solver. We apply our approach to verify safety of a set of examples, some of which cannot be proven by a first-order inductive invariant.

ABSTRACT. We study how to distribute trace languages in a setting where processes communicate via reconfigurable communication channels. That is, the different processes can connect and disconnect from channels at run time. We restrict attention to communication via tree-like communication architectures. These allow channels to connect more than two processes in a way that maintains an underlying spanning tree and keeps communication continuous on the tree. We make the reconfiguration explicit in the language allowing both a centralized automaton as well as the distributed processes to share relevant information about the current communication configuration. We show that Zielonka's seminal result regarding distribution of regular languages for asynchronous automata can be generalized in this setting, incorporating both reconfiguration and more than binary tree architectures.

ABSTRACT. In this paper, we present a stateless model checking algorithm for establishing the correctness of database backed applications modeled as transactional programs under the strongest isolation level, namely serializability. We show that our algorithm is sound, complete, optimal and runs with polynomial memory consumption. In contrast, existing DPOR algorithms for transactional programs work only with weak isolation levels exploring exponentially many more equivalence classes of executions than what serializability permits. We report an implementation of our algorithm by applying it to several thousands of litmus tests as well as challenging database backed applications from the literature.