Decision Procedures for Flat Array Properties

Francesco Alberti; Silvio Ghilardi; Natasha Sharygina

doi:10.1007/s10817-015-9323-7

Decision Procedures for Flat Array Properties

Francesco Alberti, Silvio Ghilardi, Natasha Sharygina

IRCCS Ospedale San Raffaele

Research output: Contribution to journal › Article › peer-review

Abstract

We present new decidability results for quantified fragments of theories of arrays. Our decision procedures are parametric in the theories of indexes and elements and orthogonal with respect to known results. We show that transitive closures (’acceleratio’) of relation expressing certain array updates produce formulas inside our fragment; this observation will be used to identify a class of programs handling arrays having decidable reachability problem.

Original language	English
Journal	Journal of Automated Reasoning
DOIs	https://doi.org/10.1007/s10817-015-9323-7
Publication status	Accepted/In press - Mar 20 2015

Keywords

Arrays
Decision procedures
Quantifiers
SMT

ASJC Scopus subject areas

Artificial Intelligence
Software
Computational Theory and Mathematics

Access to Document

10.1007/s10817-015-9323-7

Cite this

@article{c0de043b55fa4e818e62d173185dab6c,

title = "Decision Procedures for Flat Array Properties",

abstract = "We present new decidability results for quantified fragments of theories of arrays. Our decision procedures are parametric in the theories of indexes and elements and orthogonal with respect to known results. We show that transitive closures ({\textquoteright}acceleratio{\textquoteright}) of relation expressing certain array updates produce formulas inside our fragment; this observation will be used to identify a class of programs handling arrays having decidable reachability problem.",

keywords = "Arrays, Decision procedures, Quantifiers, SMT",

author = "Francesco Alberti and Silvio Ghilardi and Natasha Sharygina",

year = "2015",

month = mar,

day = "20",

doi = "10.1007/s10817-015-9323-7",

language = "English",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

}

TY - JOUR

T1 - Decision Procedures for Flat Array Properties

AU - Alberti, Francesco

AU - Ghilardi, Silvio

AU - Sharygina, Natasha

PY - 2015/3/20

Y1 - 2015/3/20

N2 - We present new decidability results for quantified fragments of theories of arrays. Our decision procedures are parametric in the theories of indexes and elements and orthogonal with respect to known results. We show that transitive closures (’acceleratio’) of relation expressing certain array updates produce formulas inside our fragment; this observation will be used to identify a class of programs handling arrays having decidable reachability problem.

AB - We present new decidability results for quantified fragments of theories of arrays. Our decision procedures are parametric in the theories of indexes and elements and orthogonal with respect to known results. We show that transitive closures (’acceleratio’) of relation expressing certain array updates produce formulas inside our fragment; this observation will be used to identify a class of programs handling arrays having decidable reachability problem.

KW - Arrays

KW - Decision procedures

KW - Quantifiers

KW - SMT

UR - http://www.scopus.com/inward/record.url?scp=84925263916&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84925263916&partnerID=8YFLogxK

U2 - 10.1007/s10817-015-9323-7

DO - 10.1007/s10817-015-9323-7

M3 - Article

AN - SCOPUS:84925263916

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

ER -

Decision Procedures for Flat Array Properties

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this