Treffer: Strategies for combining decision procedures

Title:
Strategies for combining decision procedures
Authors:
CONCHON, Sylvain, KRSTIC, Sava
Source:
Tools and algorithms for the construction and analysis of systems (TACAS 2003)Theoretical computer science. 354(2):187-210
Publisher Information:
Amsterdam: Elsevier, 2006.
Publication Year:
2006
Physical Description:
print, 35 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences et techniques communes, Sciences and techniques of general use, Mathematiques, Mathematics, Analyse numérique. Calcul scientifique, Numerical analysis. Scientific computation, Analyse numérique, Numerical analysis, Méthodes numériques en programmation mathématique, optimisation et calcul variationnel, Numerical methods in mathematical programming, optimization and calculus of variations, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Algorithmique. Calculabilité. Arithmétique ordinateur, Algorithmics. Computability. Computer arithmetics, Expression régulière, Regular expression, Expresión regular, Informatique théorique, Computer theory, Informática teórica, Non déterminisme, Non determinism, No determinismo, Optimisation, Optimization, Optimización, Stratégie, Strategy, Estrategia, Algorithme Shostak, Shostak algorithm, Combinaison Nelson Oppen, Nelson Oppen combination, Procédure décision, Système inférence, Inference system, Decision procedures, Inference systems, Nelson-Oppen combination, Shostak's algorithm
Document Type:
Konferenz Conference Paper
File Description:
text
Language:
English
Author Affiliations:
Laboratoire de Recherche en Informatique, Université Paris-Sud, Orsay, France
Strategic CAD Labs, Intel Corporation, Hillsboro, Oregon, United States
ISSN:
0304-3975
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=17634825
Rights:
Copyright 2006 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems

Mathematics
Accession Number:
edscal.17634825
Database:
PASCAL Archive

Weitere Informationen

Implementing efficient algorithms for combining decision procedures has been a challenge and their correctness precarious. In this paper we describe an inference system that has the classical Nelson-Oppen procedure at its core and includes several optimizations: variable abstraction with sharing, canonization of terms at the theory level, and Shostak's streamlined generation of new equalities for theories with solvers. The transitions of our system are fine-grained enough to model most of the mechanisms currently used in designing combination procedures. In particular, with a simple language of regular expressions we are able to describe several combination algorithms as strategies for our inference system, from the basic Nelson-Oppen to the very highly optimized one recently given by Shankar and Rueß. Presenting the basic system at a high level of generality and non-determinism allows transparent correctness proofs that can be extended in a modular fashion when new features are introduced in the system.