Levels of Infrastructure
First we need to distinguish between different levels of infrastructure:
We distinguish between local and distributed infrastructure.
Local infrastructure is the infrastructure that is available on the local machine. Notable examples are BenchExec and CoVeriTeam. Both are tools that make running verification tools on you machine easier. They achieve this by providing a common interface to the verification tools, serving as a layer of abstraction, between the user and the underlying tool.
Distributed infrastructure on the other hand is decoupled from the local environment. It consists mostly of services reachable over the network. A noticeable example is CoVeriTeam Service.
CPAdaemon
When running cooperative approaches like C-CEGAR the same tool is restarted over an over again. For large tools like CPAchecker this can incur a lot of overhead. CPAdaemon is a tool that aims to reduce this overhead by keeping the tool running. We reuse the same JVM, mitigating startup overhead.
Having this daemon, we also want to reuse internal components of CPAchecker:
We identify three components that are reused:
-
The parse artifact CFA. This is the stateless representation of the input program as a control flow automaton.
-
The Algorithm. These are the stateless components of the verification algorithm. From reusing we hope to get some transient effects like caching by the JVM and JIT compilation. We also reduce overhead from the reflection done when configuring the algorithm objects.
-
The Reached Set. A successful run of CPAchecker fills this reached set with states that are deemed reachable by the analysis. For some iterative approaches we want to reuse the reached set from previous runs, speeding up the reverification through information from the previous run.
CoVeriTeam Service
This work was published at ICSE '23
The research community has developed numerous tools for solving verification problems, but we are missing a common web interface for executing them. This means, users have to commit to install and execute each new tool (version) on their local machine. We propose to use CoVeriTeam Service to make it easy for verification researchers to experiment with new verification tools. CoVeriTeam has already unified the command-line interface, and reduced the burden by taking care of tool installation and isolated execution. The new web service in addition enables tool developers to make their tools accessible on the web and users to include verification tools in their work flow. There are already further applications of our service: The 2023 competitions on software verification and testing used the service for their integration testing, and we CoVeriTeam Service for incremental verification as part of a continuous-integration process.