CPA-Daemon: Mitigating Tool Restarts for Java-Based Verifiers
摘要
We present 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 that abstracts from three different modes of execution: (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. The last two are novel execution modes that greatly improve the response time of verification in different verification scenarios and enable the seamless integration of CPAchecker as an 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 https://gitlab.com/sosy-lab/software/cpa-daemon .