Certificate-Based Verification and Synthesis: Tools and Benchmarks


Listed below are some freely available tools that enable certificate-based verification by providing quantifier elimination and/or simplification capabilities on nonlinear formulas. Reduce/Redlog can now call qepcad for performing quantifier elimination.

Exists-Forall Benchmarks

Certificates for verification and synthesis can be generated by solving exists-forall formulas. Here are some exists-forall benchmarks thus generated. They are provided as reduce/redlog input files.

Exists Benchmarks

Generated by HybridSal relational abstracter and SAL infinite bounded model checker


Publications on Certificate-Based Verification and Synthesis Papers by other groups on certificate-based verification:



This material is based upon work supported in part by the National Science Foundation under Grant No. 0917398 and Grant No. 1017483. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.
This page is maintained by Ashish Tiwari.
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page