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

Konstantinos A. Athanasiou konathan at ccs.neu.edu
Sun Nov 16 22:14:52 EST 2014


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


More information about the Pl-sem-jr mailing list