CP 2016 has ended
Back To Schedule
Monday, September 5 • 10:30 - 11:05
CP meets Verification - Invited talk: Model-Constructing Satisfiabilty Calculus
    See presentations
I'll present the MCSAT approach to solving satisfiability modulo theory (SMT) problems. The MCSAT framework builds on the ideas found in modern CDCL-style SAT solvers and generalizes them to first-order setting. Although the main ideas in MCSAT come from SAT solving, in the first-order setting there are many connections to CP: a MCSAT solver operates over a domain where it maintains local consistency using dedicated propagators. The appeal of the new approach is its simplicity, deductive power, extensibility, and effectiveness on real-world problems. MCSAT has been very successful in attacking complex domains such as non-linear real and integer arithmetic.

avatar for Dejan Jovanovic

Dejan Jovanovic

SRI International
Dejan Jovanović is a computer scientist in the Computer Science Laboratory at SRI International. His research interests are automated reasoning, satisfiability, and model-checking. He is involved in development of Yices2 and CVC4 SMT solvers. He received his Ph.D. degree in computer... Read More →

Monday September 5, 2016 10:30 - 11:05
B202 Bosco building

Attendees (6)