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. © 2009 Springer.
Cite
CITATION STYLE
Seghir, M. N., Podelski, A., & Wies, T. (2009). Abstraction refinement for quantified array assertions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5673 LNCS, pp. 3–18). https://doi.org/10.1007/978-3-642-03237-0_3
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
