A new acceleration-based combination framework for array properties

Francesco Alberti, Silvio Ghilardi, Natasha Sharygina

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

Abstract

This paper presents an acceleration-based combination framework for checking the satisfiability of classes of quantified formulæ of the theory of arrays. We identify sufficient conditions for which an ‘acceleratability’ result can be used as a black-box module inside such satisfiability procedures. Besides establishing new decidability results and relating them to results from recent literature, we discuss the application of our combination framework to the problem of checking the safety of imperative programs with arrays.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer Verlag
Pages169-185
Number of pages17
Volume9322
ISBN (Print)9783319242453
DOIs
Publication statusPublished - 2015
Event10th International Symposium on Frontiers of Combining Systems, FroCoS 2015 - Wroclaw, Poland
Duration: Sep 21 2015Sep 24 2015

Publication series

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

Other

Other10th International Symposium on Frontiers of Combining Systems, FroCoS 2015
Country/TerritoryPoland
CityWroclaw
Period9/21/159/24/15

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Fingerprint

Dive into the research topics of 'A new acceleration-based combination framework for array properties'. Together they form a unique fingerprint.

Cite this