[Pl-seminar] Fwd: Talk Announcement: Clark Barrett "New Insights on the Nelson-Oppen Method" Monday, August 13th at 11:00am

[Aaron Turon]

This talk is hosted by the formal methods group, but will likely be of
interest to the PL community as well.

---------- Forwarded message ----------
From: Nicole Bekerian <nicoleb at ccs.neu.edu>
Date: Thu, Aug 9, 2012 at 2:29 PM
Subject: [phds] [Colloq] Talk Announcement: Clark Barrett "New
Insights on the Nelson-Oppen Method" Monday, August 13th at 11:00am
To: colloq <colloq at lists.ccs.neu.edu>

The College of Computer and Information Science presents:

Title: New Insights on the Nelson-Oppen Method
Speaker: Clark Barrett, New York University
Coordinates: Monday, August 13, 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.