Speaker: Edmund Clarke

Title: SMT Solving for Nonlinear Theories over the Reals

 

We describe our open-source tool dReal, an SMT solver for nonlinear formulas over the reals. The tool can handle various nonlinear real functions such as polynomials, trigonometric functions,

exponential functions, etc. dReal implements the framework of delta-complete decision procedures: It returns either unsat or delta-sat on input formulas, where delta is a numerical error bound specified by the user. When the answer is unsat, dReal produces a proof of unsatisfiability; when delta-sat, it provides a solution that witnesses the satisfiability of a delta-perturbed form of the input formula. With such relaxation, delta-complete decision procedures can fully exploit the power of scalable numerical algorithms to solve nonlinear problems, and at the same time provide suitable correctness guarantees for various correctness-critical problems.

 

 

 

Edmund Clarke is professor at Carnegie Mellon University where he holds an endowed chair in the School of Computer Science.

 

Clarke's interests include software and hardware verification and automatic theorem proving. In 1981 he and his Ph.D. student E. Allen Emerson first proposed the use of model checking as a verification technique for finite state concurrent systems, with application to hardware verification.  With Randal Bryant, E. Allen Emerson, and Kenneth McMillan, he also initiated the development of symbolic model checking, for which they received the prestigious ACM Paris Kanellakis Award in 1999. In 2004 he received the IEEE Computer Society Harry H. Goode Memorial Award for significant and pioneering contributions to formal verification of hardware and software systems, and for the profound impact these contributions have had on the electronics industry. He, Alan Emerson and Joseph Sifakis received the prestigious Turing award for their pionneering achievements on model checking in 2007. He also received the Herbrand award in 2008. In 2009, he led the creation of the Computational Modeling and Analysis of Complex Systems center, funded by the National Science Foundation. This center spans multiple universities, applying abstract interpretation and model checking to biological and embedded systems.

 

Edmund Clarke is a member of the American Academies of Engineering and of Art and Sciences, and a fellow of the ACM and IEEE.