Candidate: Dejan Jovanovic
Advisors: Clark Barrett

Committee:
Prof. Clark Barrett(NYU CS Advisor, Reader)
Dr. Leonardo de Moura(Microsoft Research,Reader)
Prof. Thomas Weis (NYU CS, Reader)
Prof. Benjamin Goldberg (NYU, Auditor)
Prof. Morgan Deters, (NYU Auditor)

Time: Thursday Sept. 13, 10:00am

Place: Warren Weaver Hall (Room 412)

Title: SMT Beyond DPLL(T): A New Approach to Theory Solvers and Theory Combination

Abstract: Satisifiability modulo theories (SMT) is the problem of deciding whether a given logical formula can be satisifed with respect to a combination of background theories. The past few decades have seen many significant developments in the field, including fast Boolean satisfiability solvers (SAT), efficient decision procedures for a growing number of expressive theories, and frameworks for modular combination of decision procedures. All these improvements, with addition of robust SMT solver implementations, culminated with the acceptance of SMT as a standard tool in the fields of automated reasoning and computer aided verification. In this thesis we develop new decision procedures for the theory of linear integer arithmetic and the theory of non-linear real arithmetic, and develop a new general framework fro combination of decision procedures. The new decision procedures integrate theory specific reasoning and the Boolean search to provide more powerful and efficient procedures, and allow a more expressive language for explaining problematic states. The new framework for combination of decision procedures overcomes the complexity limitations and restrictions on the theories imposed by the standard Nelson-Oppen approach.