---

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 available at gitlab.com/sosy-lab/software/cpa-daemon.

---

Tool and Reproduction Information

A reproduction package of this work is available on Zenodo (). The implementation of CPA-Daemon is available on GitLab.

---

Full Results

The experimental results reported in the paper can be seen in the interactive tables below.

• RQ 1: Does CPA-Daemon produce results that are consistent with CPAchecker, and RQ 2: Are the CPA-Daemon backends 'Native Execution' and 'Library' more efficient than backend 'Separate JVM'?
• RQ 3: Can cooperative verification approaches benefit from CPA-Daemon, compared to off-the-shelf CPAchecker?