Decision procedures for extensions of the theory of arrays
Identifieur interne : 004C79 ( Main/Exploration ); précédent : 004C78; suivant : 004C80Decision procedures for extensions of the theory of arrays
Auteurs : Silvio Ghilardi [Italie] ; Enrica Nicolini [France] ; Silvio Ranise [France] ; Daniele Zucchelli [Italie, France]Source :
- Annals of Mathematics and Artificial Intelligence [ 1012-2443 ] ; 2007-08-01.
English descriptors
- KwdEn :
Abstract
Abstract: The theory of arrays, introduced by McCarthy in his seminal paper “Towards a mathematical science of computation,” is central to Computer Science. Unfortunately, the theory alone is not sufficient for many important verification applications such as program analysis. Motivated by this observation, we study extensions of the theory of arrays whose satisfiability problem (i.e., checking the satisfiability of conjunctions of ground literals) is decidable. In particular, we consider extensions where the indexes of arrays have the algebraic structure of Presburger arithmetic and the theory of arrays is augmented with axioms characterizing additional symbols such as dimension, sortedness, or the domain of definition of arrays. We provide methods for integrating available decision procedures for the theory of arrays and Presburger arithmetic with automatic instantiation strategies which allow us to reduce the satisfiability problem for the extension of the theory of arrays to that of the theories decided by the available procedures. Our approach aims to re-use as much as possible existing techniques so as to ease the implementation of the proposed methods. To this end, we show how to use model-theoretic, rewriting-based theorem proving (i.e., superposition), and techniques developed in the Satisfiability Modulo Theories communities to implement the decision procedures for the various extensions.
Url:
DOI: 10.1007/s10472-007-9078-x
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 003C18
- to stream Istex, to step Curation: 003B74
- to stream Istex, to step Checkpoint: 001064
- to stream Hal, to step Corpus: 001B14
- to stream Hal, to step Curation: 001B14
- to stream Hal, to step Checkpoint: 003D81
- to stream Main, to step Merge: 004E13
- to stream Main, to step Curation: 004C79
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Decision procedures for extensions of the theory of arrays</title><author><name sortKey="Ghilardi, Silvio" sort="Ghilardi, Silvio" uniqKey="Ghilardi S" first="Silvio" last="Ghilardi">Silvio Ghilardi</name></author><author><name sortKey="Nicolini, Enrica" sort="Nicolini, Enrica" uniqKey="Nicolini E" first="Enrica" last="Nicolini">Enrica Nicolini</name></author><author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name></author><author><name sortKey="Zucchelli, Daniele" sort="Zucchelli, Daniele" uniqKey="Zucchelli D" first="Daniele" last="Zucchelli">Daniele Zucchelli</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:FADECB736AA1A004528ECCA6647F10E187F15EAB</idno><date when="2007" year="2007">2007</date><idno type="doi">10.1007/s10472-007-9078-x</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-R9Z4TGN9-9/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003C18</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003C18</idno><idno type="wicri:Area/Istex/Curation">003B74</idno><idno type="wicri:Area/Istex/Checkpoint">001064</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001064</idno><idno type="wicri:doubleKey">1012-2443:2007:Ghilardi S:decision:procedures:for</idno><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:inria-00576588</idno><idno type="url">https://hal.inria.fr/inria-00576588</idno><idno type="wicri:Area/Hal/Corpus">001B14</idno><idno type="wicri:Area/Hal/Curation">001B14</idno><idno type="wicri:Area/Hal/Checkpoint">003D81</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">003D81</idno><idno type="wicri:doubleKey">1012-2443:2007:Ghilardi S:decision:procedures:for</idno><idno type="wicri:Area/Main/Merge">004E13</idno><idno type="wicri:Area/Main/Curation">004C79</idno><idno type="wicri:Area/Main/Exploration">004C79</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Decision procedures for extensions of the theory of arrays</title><author><name sortKey="Ghilardi, Silvio" sort="Ghilardi, Silvio" uniqKey="Ghilardi S" first="Silvio" last="Ghilardi">Silvio Ghilardi</name><affiliation wicri:level="3"><country xml:lang="fr">Italie</country><wicri:regionArea>Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano, Milan</wicri:regionArea><placeName><settlement type="city">Milan</settlement><region nuts="2">Lombardie</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Italie</country></affiliation></author><author><name sortKey="Nicolini, Enrica" sort="Nicolini, Enrica" uniqKey="Nicolini E" first="Enrica" last="Nicolini">Enrica Nicolini</name><affiliation wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>LORIA & INRIA-Lorraine, Nancy Cedex</wicri:regionArea><wicri:noRegion>Nancy Cedex</wicri:noRegion><wicri:noRegion>Nancy Cedex</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name><affiliation wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>LORIA & INRIA-Lorraine, Nancy Cedex</wicri:regionArea><wicri:noRegion>Nancy Cedex</wicri:noRegion><wicri:noRegion>Nancy Cedex</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Zucchelli, Daniele" sort="Zucchelli, Daniele" uniqKey="Zucchelli D" first="Daniele" last="Zucchelli">Daniele Zucchelli</name><affiliation wicri:level="3"><country xml:lang="fr">Italie</country><wicri:regionArea>Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano, Milan</wicri:regionArea><placeName><settlement type="city">Milan</settlement><region nuts="2">Lombardie</region></placeName></affiliation><affiliation wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>LORIA & INRIA-Lorraine, Nancy Cedex</wicri:regionArea><wicri:noRegion>Nancy Cedex</wicri:noRegion><wicri:noRegion>Nancy Cedex</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Italie</country></affiliation></author></analytic><monogr></monogr><series><title level="j">Annals of Mathematics and Artificial Intelligence</title><title level="j" type="abbrev">Ann Math Artif Intell</title><idno type="ISSN">1012-2443</idno><idno type="eISSN">1573-7470</idno><imprint><publisher>Springer Netherlands</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="2007-08-01">2007-08-01</date><biblScope unit="volume">50</biblScope><biblScope unit="issue">3-4</biblScope><biblScope unit="page" from="231">231</biblScope><biblScope unit="page" to="254">254</biblScope></imprint><idno type="ISSN">1012-2443</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">1012-2443</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Combination methods</term><term>Constraint satisfiability problems</term><term>Decision procedures</term><term>Instantiation strategies</term><term>Presburger arithmetic</term><term>Theory of arrays with extensionality</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: The theory of arrays, introduced by McCarthy in his seminal paper “Towards a mathematical science of computation,” is central to Computer Science. Unfortunately, the theory alone is not sufficient for many important verification applications such as program analysis. Motivated by this observation, we study extensions of the theory of arrays whose satisfiability problem (i.e., checking the satisfiability of conjunctions of ground literals) is decidable. In particular, we consider extensions where the indexes of arrays have the algebraic structure of Presburger arithmetic and the theory of arrays is augmented with axioms characterizing additional symbols such as dimension, sortedness, or the domain of definition of arrays. We provide methods for integrating available decision procedures for the theory of arrays and Presburger arithmetic with automatic instantiation strategies which allow us to reduce the satisfiability problem for the extension of the theory of arrays to that of the theories decided by the available procedures. Our approach aims to re-use as much as possible existing techniques so as to ease the implementation of the proposed methods. To this end, we show how to use model-theoretic, rewriting-based theorem proving (i.e., superposition), and techniques developed in the Satisfiability Modulo Theories communities to implement the decision procedures for the various extensions.</div></front></TEI><affiliations><list><country><li>France</li><li>Italie</li></country><region><li>Lombardie</li></region><settlement><li>Milan</li></settlement></list><tree><country name="Italie"><region name="Lombardie"><name sortKey="Ghilardi, Silvio" sort="Ghilardi, Silvio" uniqKey="Ghilardi S" first="Silvio" last="Ghilardi">Silvio Ghilardi</name></region><name sortKey="Ghilardi, Silvio" sort="Ghilardi, Silvio" uniqKey="Ghilardi S" first="Silvio" last="Ghilardi">Silvio Ghilardi</name><name sortKey="Zucchelli, Daniele" sort="Zucchelli, Daniele" uniqKey="Zucchelli D" first="Daniele" last="Zucchelli">Daniele Zucchelli</name><name sortKey="Zucchelli, Daniele" sort="Zucchelli, Daniele" uniqKey="Zucchelli D" first="Daniele" last="Zucchelli">Daniele Zucchelli</name></country><country name="France"><noRegion><name sortKey="Nicolini, Enrica" sort="Nicolini, Enrica" uniqKey="Nicolini E" first="Enrica" last="Nicolini">Enrica Nicolini</name></noRegion><name sortKey="Nicolini, Enrica" sort="Nicolini, Enrica" uniqKey="Nicolini E" first="Enrica" last="Nicolini">Enrica Nicolini</name><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name><name sortKey="Zucchelli, Daniele" sort="Zucchelli, Daniele" uniqKey="Zucchelli D" first="Daniele" last="Zucchelli">Daniele Zucchelli</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004C79 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 004C79 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:FADECB736AA1A004528ECCA6647F10E187F15EAB
|texte= Decision procedures for extensions of the theory of arrays
}}
| This area was generated with Dilib version V0.6.33. |  |