Definability of accelerated relations in a theory of arrays and its applications

Francesco Alberti, Silvio Ghilardi, Natasha Sharygina

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

For some classes of guarded ground assignments for arrays, we show that accelerations (i.e. transitive closures) are definable in the theory of arrays via ∃*∀*-first order formulae. We apply this result to model checking of unbounded array programs, where the computation of such accelerations can be used to prevent divergence of reachability analysis. To cope with nested quantifiers introduced by acceleration preprocessing, we use simple instantiation and refinement strategies during backward search analysis. Our new acceleration technique and abstraction/refinement loops are mutually beneficial: experiments conducted with the SMT-based model checker mcmt attest the effectiveness of our approach where acceleration and abstraction/refinement technologies fail if applied alone.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages23-39
Number of pages17
Volume8152 LNAI
DOIs
Publication statusPublished - 2013
Event9th International Symposium on Frontiers of Combining Systems, FroCoS 2013 - Nancy, France
Duration: Sep 18 2013Sep 20 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8152 LNAI
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other9th International Symposium on Frontiers of Combining Systems, FroCoS 2013
CountryFrance
CityNancy
Period9/18/139/20/13

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Fingerprint Dive into the research topics of 'Definability of accelerated relations in a theory of arrays and its applications'. Together they form a unique fingerprint.

  • Cite this

    Alberti, F., Ghilardi, S., & Sharygina, N. (2013). Definability of accelerated relations in a theory of arrays and its applications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8152 LNAI, pp. 23-39). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8152 LNAI). https://doi.org/10.1007/978-3-642-40885-4_3