Abstraction Refinement for Quantified Array Assertions

ion Refinement for Quantified Array Assertions Mohamed Nassim Seghir1, , Andreas Podelski1 , and Thomas Wies1,2 1 University of Freiburg, Germany 2 EPFL, Switzerland 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.

• Type: Conference
• Year: 2009
• Where: SAS
• Authors: Mohamed Nassim Seghir, Andreas Podelski, Thomas Wies
• Keywords: Abstraction Refinement Technique, Formal Methods, Model Checking Algorithms, Quantified Array Assertions, SAS 2009