Le séminaire du LSV

Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Stéphane Le Roux and Matthias Fuegger.

Le séminaire du LSV est public et ne nécessite aucune inscription préalable.

Séminaires passés

The CVC4 SMT Solver

Visiter le site web pour cet événement | Exporter cet événement au format iCalendar

 Morgan Deters
Date
Le mardi 04 novembre 2014 à 11:00
Lieu
Salle de Conférence (Pavillon des Jardins)
Orateur
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.


À propos du LSV

Agenda des séminaires

Exporter l'agenda au format iCalendar | Les séminaires précédents

mar. 19 février

Les séminaires précédents