Decision Procedures for Flat Array Properties

Francesco Alberti, Silvio Ghilardi, Natasha Sharygina

Research output: Contribution to journalArticlepeer-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 languageEnglish
JournalJournal of Automated Reasoning
DOIs
Publication statusAccepted/In press - Mar 20 2015

Keywords

  • Arrays
  • Decision procedures
  • Quantifiers
  • SMT

ASJC Scopus subject areas

  • Artificial Intelligence
  • Software
  • Computational Theory and Mathematics

Fingerprint Dive into the research topics of 'Decision Procedures for Flat Array Properties'. Together they form a unique fingerprint.

Cite this