CVC4 tutorial to run at CADE-24

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:

  • how to encode a variety of verification problems as SMT queries;
  • how to develop and run SMT-LIB command scripts;
  • how to run CVC4 interactively from the command line;
  • how to use CVC4 as a programming library;
  • common problems encountered when using SMT solvers; and
  • selected details about what goes on “under the hood” in an SMT solver.

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.