Predicate Pairing for Program Verification

This page includes supplementary material for the Experimental evaluation.

• CHCsBPP - CHCs Before Predicate Pairing (CHCs encodings of the verification problems and their representation in SMT-LIB format)
• Statistics on the satisfiability check for CHCsBPP (Z3 with Duality)
• CHCsAPP - CHCs After Predicate Pairing (transformed CHCs, transformed CHCs in SMT-LIB format, and transformation logs) - Statistics on the transformation process.
• Statistics on the satisfiability check for CHCsAPP (Z3 with Duality)

Additional material

• Details on the VCs generation can be found here
• C sources for a subset of the benchmark set