MPI-INF Logo
Publications

Server    domino.mpi-inf.mpg.de

Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop

Author, Editor
Author(s):
Lynch, Christopher
Tran, Duc-Khanh		dblp
dblp
Not MPG Author(s):
Lynch, Christopher
Editor(s):
Cha, Sungdeok (Steve)
Choi, Jin-Young
Kim Moonzoo
Lee, Insup
Viswanathan, Mahesh		dblp
dblp
dblp
dblp
dblp
Not MPII Editor(s):
Cha, Sungdeok (Steve)
Choi, Jin-Young
Kim Moonzoo
Lee, Insup
Viswanathan, Mahesh
BibTeX cite key*:
tran-atva08
Title, Booktitle
Title*:
SMELS: Satisfiability Modulo Equality with Lazy Superposition
Booktitle*:
Automated Technology for Verification and Analysis 6th International Symposium, ATVA 2008
Event, URLs
Conference URL::
http://pswlab.kaist.ac.kr/atva2008/
Downloading URL:
http://www.springerlink.com/content/x58h1487t724k2l0/
Event Address*:
Seoul, Korea
Language:
English
Event Date*
(no longer used):
Organization:
Event Start Date:
20 October 2008
Event End Date:
23 October 2008
Publisher
Name*:
Springer
URL:
http://www.springer-ny.com/
Address*:
Berlin / Heidelberg
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Computer Science
Volume:
5311
Number:
Month:
Pages:
186-200
Year*:
2008
VG Wort Pages:
ISBN/ISSN:
0302-9743
Sequence Number:
DOI:
Note, Abstract, ©
(LaTeX) Abstract:
We give a method for extending efficient SMT solvers to handle quantifiers, using Superposition inference rules. In our method, the input formula is converted into CNF as in traditional first order logic theorem provers. The ground clauses are given to the SMT solver, which runs a DPLL method to build partial models. The partial model is passed to a Congruence Closure procedure, as is normally done in SMT. Congruence Closure calculates all reduced (dis)equations in the partial model and passes them to a Superposition procedure, along with a justification. The Superposition procedure then performs an inference rule, which we call Justified Superposition, between the (dis)equations and the nonground clauses, plus usual Superposition rules with the nonground clauses. Any resulting ground clauses are provided to the DPLL engine. We prove the completeness of this method, using a nontrivial modification of Bachmair and Ganzinger’s model generation technique. We believe this combination uses the best of both worlds, an SMT process to handle ground clauses efficiently, and a Superposition procedure which uses orderings to handle the nonground clauses.
URL for the Abstract:
http://www.springerlink.com/content/x58h1487t724k2l0/
Download
Access Level:
Public

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Automation of Logic
Audience:
experts only
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:

@INPROCEEDINGS{tran-atva08,
AUTHOR = {Lynch, Christopher and Tran, Duc-Khanh},
 EDITOR = {Cha, Sungdeok (Steve) and Choi, Jin-Young and Kim Moonzoo and Lee, Insup and Viswanathan, Mahesh},
 TITLE = {{SMELS}: Satisfiability Modulo Equality with Lazy Superposition},
 BOOKTITLE = {Automated Technology for Verification and Analysis 6th International Symposium, ATVA 2008},
 PUBLISHER = {Springer},
 YEAR = {2008},
 VOLUME = {5311},
 PAGES = {186--200},
 SERIES = {Lecture Notes in Computer Science},
 ADDRESS = {Seoul, Korea},
 ISBN = {0302-9743},
}

Entry last modified by Uwe Waldmann, 03/01/2013
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Viorica Sofronie-Stokkermans		Created
03/06/2009 12:59:09 PM
Revisions
2.
1.
0.

Editor(s)
Uwe Waldmann
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans

Edit Dates
01.03.2013 11:25:25
03/06/2009 12:59:53 PM
03/06/2009 12:59:09 PM