Abstraction refinement for quantified array assertions

Mohamed Nassim Seghir, Andreas Podelski, Thomas Wies

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


We present an abstraction refinement technique for the verification of universally quantified array assertions such as "all elements in the array are sorted". Our technique can be seamlessly combined with existing software model checking algorithms. We implemented our technique in the ACSAR software model checker and successfully verified quantified array assertions for both text book examples and real-life examples taken from the Linux operating system kernel.

Original languageEnglish (US)
Title of host publicationStatic Analysis - 16th International Symposium, SAS 2009, Proceedings
Number of pages16
StatePublished - 2009
Event16th International Symposium on Static Analysis, SAS 2009 - Los Angeles, CA, United States
Duration: Aug 9 2009Aug 11 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5673 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other16th International Symposium on Static Analysis, SAS 2009
Country/TerritoryUnited States
CityLos Angeles, CA

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Abstraction refinement for quantified array assertions'. Together they form a unique fingerprint.

Cite this