LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Past Seminars
The CVC4 SMT Solver
- Date
- Tuesday, November 04 2014 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- Morgan Deters (New York University)
Satisfiability Modulo Theories (SMT) solvers leverage research advances in SAT solving and decision procedures to solve Boolean combinations of constraints written in an expressive language combining different background theories. CVC4 is a solver for these SMT problems with a number of features useful in verification, static analysis, synthesis, symbolic execution, and other domains. This talk provides an overview of SMT and describes the main features of SMT solvers, with a focus on CVC4. I discuss various aspects of CVC4's internals, including its architecture, its capacity for dealing with quantifiers, its finite model finder, and the linear arithmetic solver. CVC4, jointly developed at New York University and the University of Iowa, is freely available for both research and commercial use under an open-source license.