A Circuit-based Program Verifier for C System Requirements CPV relies on CoVeriTeam to coordinate the underlying hardware verifiers. Therefore, the following dependencies are required: Linux Ubuntu 22.04 or newer Python 3.10 or newer Control groups (cgroups) The complete dependencies of CoVeriTeam can be found in its documentation. Additional required Python packages are listed in requirements.txt. Usage To verify whether a C program (c_prog) satisfies the given property (specified by prp_file), run: ./bin/cpv --property --model {ILP32,LP64} Please refer to ./bin/cpv -h for more information. License CPV uses Kratos2 (in kratos2/) to translate C programs, utility tools and libraries for Btor2, AIGER, and VMT (in bin/ and lib/) to manipulate circuits, and hardware model checkers (in cvt-cache/) for verification. Their cooperation is implemented with the CoVeriTeam library (in lib/). The above tools are available under their respective licenses. Other components of CPV, including program instrumentor, functional encoder, witness translator, and portfolio executor, are licensed under the Apache 2.0 License. References CPV: A Circuit-Based Program Verifier (Competition Contribution), by Po-Chun Chien and Nian-Ze Lee. In Proc. TACAS. Springer (2024).