[Colloq] Reminder: Talk Announcement: Clark Barrett "New Insights on the Nelson-Oppen Method" Today at 11:00am

[Nicole Bekerian]

The College of Computer and Information Science presents:

Title: New Insights on the Nelson-Oppen Method
Speaker: Clark Barrett, New York University
Coordinates: Today, 11AM, WVH 366
Host: Pete Manolios

Abstract:
In the past decade, there has been a steady increase in the use of formal methods to verify systems.  First-order theories provide a nice balance between expressive power and computational tractability, and for this reason, SMT solvers have become the tool of choice for many verification tasks.

SMT verification conditions often need to combine reasoning about several theories.
The Nelson-Oppen method is the key to theory combination in SMT solvers.  In this talk, I will briefly review Nelson-Oppen and then discuss two
extensions: one
which allows combinations with non-stably-infinite theories (allowing arrays of bit-vectors for example) and one which improves the effieciency of the basic Nelson-Oppen step of computing arrangements by computing care functions for each theory.


-- 




Best, 
Nicole 

______________________________________________________________ 

Nicole Bekerian 
Administrative Assistant 

Northeastern University 
College of Computer and Information Science 
360 Huntington Ave. 
202 West Village H 
Boston, MA 02115 

Phone: 617.373.2462 
Fax: 617.373.5121