Campus Event Calendar
Event Entry
New for: D3
What and Who
Combining Satisfiability Procedures for Unions of Theories Sharing Fragments of Arithmetic
Christophe Ringeissen
INRIA, Nancy
Talk
AG 1, AG 3, AG 4, AG 5, SWS, RG1, MMCI
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 30 April 2010
14:15
60 Minutes
E1 4
024
Saarbrücken
Abstract
We show how to apply a non-disjoint extension of the Nelson-Oppen
combination method to develop a decision procedure for the union of
theories sharing some arithmetic operators. Different possible
shared theories are discussed: two possible axiomatisations for
counter arithmetic, and the theory of abelian groups. We present
theories modelling some data-structures for which the combination
method is complete and effective. To achieve effectiveness, the
combination method relies on particular procedures to compute sets
that are representative of all the consequences over the shared
theory. We show how to compute these sets by using an appropriate
superposition calculus and a careful adaptation of standard methods
for reasoning about arithmetic. We discuss the underlying
implementation issues and the possible integration of the
non-disjoint combination method into a SMT solver.
combination method to develop a decision procedure for the union of
theories sharing some arithmetic operators. Different possible
shared theories are discussed: two possible axiomatisations for
counter arithmetic, and the theory of abelian groups. We present
theories modelling some data-structures for which the combination
method is complete and effective. To achieve effectiveness, the
combination method relies on particular procedures to compute sets
that are representative of all the consequences over the shared
theory. We show how to compute these sets by using an appropriate
superposition calculus and a careful adaptation of standard methods
for reasoning about arithmetic. We discuss the underlying
implementation issues and the possible integration of the
non-disjoint combination method into a SMT solver.
Contact
Jennifer Müller
9325-900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 04/16/2010 13:11 -- Created document.