Abstraction Refinement for Quantified Array Assertions

Mohamed Nassim Seghir, Andreas Podelski, Thomas Wies

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

Abstract

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
Title of host publicationStatic Analysis
Subtitle of host publication16th International Symposium, SAS 2009, Los Angeles, CA, USA, August 9-11, 2009. Proceedings
PublisherSpringer Berlin Heidelberg
Pages3-18
Number of pages16
Volume5673
ISBN (Electronic)978-3-642-03237-0
ISBN (Print)978-3-642-03236-3
DOIs
Publication statusPublished - 2009

Fingerprint

Dive into the research topics of 'Abstraction Refinement for Quantified Array Assertions'. Together they form a unique fingerprint.

Cite this