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!


CI

12 December 2012

CVC4 Tutorial to Run at CADE-24

by Morgan Deters

Our tutorial entitled “Becoming a power user of SMT: The CVC4 solver, how it works, and how best to use it” was just accepted to run at CADE-24 in June 2013 in Lake Placid, NY. We are excited to have the opportunity to demonstrate the capabilities of CVC4 and to use it as a teaching device.

Planned topics to cover include:

This tutorial will turn casual users of SMT into users capable of encoding complex, real-world problems in SMT and effectively tuning and using CVC4 to solve them.