CVC4

An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

About
News
Downloads
Documentation
Publications
Awards
People
History
Third-Party Applications
Acknowledgements

Try CVC4 online!


Solving Quantified Bit-Vectors Using Invertibility Conditions

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli

This site provides our paper Solving Quantified Bit-Vectors Using Invertibility Conditions and related material at CAV 2018.

An extended version of our paper at CAV 2018 can be found below.

All materials to reproduce the experimental evaluation in our paper can be found below.

Downloads