salle A. Turing CE4
3 March 2016 - 15h00
Introduction to SMT & JavaSMT: A Unified Library for Utilizing SMT Solvers
by George Karpenkov from VERIMAG
Abstract: The talk is split in two short parts.
The first part is by David Monniaux.
David will give an introduction to satisfiability modulo theory:
- what it is
- how solvers are used
- usual theories
- limitations
The second part is by George Karpenkov.
George will give a short talk on the newly developed JavaSMT tool (https://github.com/sosy-lab/java-smt/), which can be used for posing queries to various SMT solvers.
Comparison with the SMT-LIB2-based communication and the direct API usage will be given.
The talk will also include a short argument for using Java for building code analysis tools.
