[PL-sem-jr] A High Level Design of a SMT Solver (11/16, 12:00-1:30, 366 WVH)

[Konstantinos A. Athanasiou]

SMT has attracted research interest both in its foundations and its
applications during the last years, and SMT solvers (or SMT-like
techniques) have been used in a variety of environments such as interactive
theorem provers, model checkers and unit test generators.

In tomorrow's talk we will attempt to look into the internals of SMT
solvers, by means of the DPLL(T) abstract framework, and discuss how they
integrate the advances of modern SAT solvers with efficient theory solvers.

Konstantinos Athanasiou
-------------- next part --------------
HTML attachment scrubbed and removed