Paula Chocron
(University of Buenos Aires)
Dealing with Multiple Theories: the Combination Problem in SMT Solving
November 8th at 17:30, in ILLC Seminar Room (F1.15)
The Satisfiability Modulo Theories problem is about deciding if a first order logic formula is satisfiable with respect to background theories. Solving SMT requires combining boolean satisfiability and decision algorithms for the theories, and provides a useful tool for verifying properties over, for example, software specifications.
In this talk I will start with a general introduction (no background needed!) and then focus in the Combination Problem: what happens if we don't have just one background theory, but many of them? How can we decide satisfiability for the combination? Which theories will get along well with each other, and for which ones will it be a complete chaos? To finish, some examples of problematic cases i'm working in and ideas of how to solve them.