Certified Verification for Algebraic Abstraction

This is an artifact created for CAV 2023 submission: "Certified Verification for Algebraic Abstraction". We present a certified algebraic abstraction technique for verifying bit-accurate non-linear integer computations. Our certified algebraic abstraction is implemented in the verified model checker CoqCryptoLine. The CoqCryptoLine tool is built on the OCaml programs extracted from verified formalizations. We evaluate our algebraic abstraction on real-world cryptographic programs. This artifact contains CoqCryptoLine, CryptoLine, and benchmarks used to replicate the experimental results (Table 1) in the paper. The extracted OCaml code of CoqCryptoLine in this artifact is instrumented to report the running time of CoqQFBV