InforLorV4, Main, Merge, bibRecord, 005655

Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies

Identifieur interne : 005655 ( Main/Merge ); précédent : 005654; suivant : 005656

Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies

Auteurs : Silvio Ghilardi [Italie] ; Enrica Nicolini [Italie] ; Silvio Ranise [Italie, France] ; Daniele Zucchelli [Italie, France]

Source :

Lecture Notes in Computer Science [ 0302-9743 ]

RBID : ISTEX:C0B0245ECBE1AE666144FE0A4F656023446D24D8

Abstract

Abstract: The theory of arrays, introduced by McCarthy in his seminal paper “Toward 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 has 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 reuse as much as possible existing techniques so to ease the implementation of the proposed methods. To this end, we show how to use both model-theoretic and rewriting-based theorem proving (i.e., superposition) techniques to implement the instantiation strategies of the various extensions.

Url:

https://api.istex.fr/ark:/67375/HCB-H1JKPJRX-G/fulltext.pdf

DOI: 10.1007/11853886_16

Links toward previous steps (curation, corpus...)

to stream Istex, to step Corpus: 002D69
to stream Istex, to step Curation: 002D32
to stream Istex, to step Checkpoint: 001362

Links to Exploration step

ISTEX:C0B0245ECBE1AE666144FE0A4F656023446D24D8

Le document en format XML

<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies</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:C0B0245ECBE1AE666144FE0A4F656023446D24D8</idno>
<date when="2006" year="2006">2006</date>
<idno type="doi">10.1007/11853886_16</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-H1JKPJRX-G/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">002D69</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002D69</idno>
<idno type="wicri:Area/Istex/Curation">002D32</idno>
<idno type="wicri:Area/Istex/Checkpoint">001362</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001362</idno>
<idno type="wicri:doubleKey">0302-9743:2006:Ghilardi S:deciding:extensions:of</idno>
<idno type="wicri:Area/Main/Merge">005655</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies</title>
<author><name sortKey="Ghilardi, Silvio" sort="Ghilardi, Silvio" uniqKey="Ghilardi S" first="Silvio" last="Ghilardi">Silvio Ghilardi</name>
<affiliation wicri:level="1"><country xml:lang="fr">Italie</country>
<wicri:regionArea>Dipartimento di Informatica, Università degli Studi di Milano</wicri:regionArea>
<wicri:noRegion>Università degli Studi di Milano</wicri:noRegion>
</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">Italie</country>
<wicri:regionArea>Dipartimento di Matematica, Università degli Studi di Milano</wicri:regionArea>
<wicri:noRegion>Università degli Studi di Milano</wicri:noRegion>
</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">Italie</country>
<wicri:regionArea>Dipartimento di Informatica, Università degli Studi di Milano</wicri:regionArea>
<wicri:noRegion>Università degli Studi di Milano</wicri:noRegion>
</affiliation>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA & INRIA-Lorraine, Nancy</wicri:regionArea>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
</affiliation>
</author>
<author><name sortKey="Zucchelli, Daniele" sort="Zucchelli, Daniele" uniqKey="Zucchelli D" first="Daniele" last="Zucchelli">Daniele Zucchelli</name>
<affiliation wicri:level="1"><country xml:lang="fr">Italie</country>
<wicri:regionArea>Dipartimento di Informatica, Università degli Studi di Milano</wicri:regionArea>
<wicri:noRegion>Università degli Studi di Milano</wicri:noRegion>
</affiliation>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA & INRIA-Lorraine, Nancy</wicri:regionArea>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title>
<idno type="ISSN">0302-9743</idno>
<idno type="eISSN">1611-3349</idno>
<idno type="ISSN">0302-9743</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass></textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: The theory of arrays, introduced by McCarthy in his seminal paper “Toward 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 has 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 reuse as much as possible existing techniques so to ease the implementation of the proposed methods. To this end, we show how to use both model-theoretic and rewriting-based theorem proving (i.e., superposition) techniques to implement the instantiation strategies of the various extensions.</div>
</front>
</TEI>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 005655 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 005655 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Merge
   |type=    RBID
   |clé=     ISTEX:C0B0245ECBE1AE666144FE0A4F656023446D24D8
   |texte=   Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies

Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies

Source :

Abstract

Links toward previous steps (curation, corpus...)

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri