Abstraction refinement for quantified array assertions
Seghir M, Podelski A, Wies T. 2009. Abstraction refinement for quantified array assertions. 16th International Symposium on Static Analysis. SAS: Static Analysis Symposium, LNCS, vol. 5673, 3–18.
Download
No fulltext has been uploaded. References only!
Conference Paper
| Published
| English
Author
Seghir, Mohamed;
Podelski, Andreas;
Wies, ThomasISTA
Series Title
LNCS
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.
Publishing Year
Date Published
2009-01-01
Proceedings Title
16th International Symposium on Static Analysis
Publisher
Springer
Volume
5673
Page
3 - 18
Conference
SAS: Static Analysis Symposium
Conference Location
Los Angeles, CA, United States
Conference Date
2009-08-09 – 2009-08-11
IST-REx-ID
Cite this
Seghir M, Podelski A, Wies T. Abstraction refinement for quantified array assertions. In: 16th International Symposium on Static Analysis. Vol 5673. Springer; 2009:3-18. doi:10.1007/978-3-642-03237-0_3
Seghir, M., Podelski, A., & Wies, T. (2009). Abstraction refinement for quantified array assertions. In 16th International Symposium on Static Analysis (Vol. 5673, pp. 3–18). Los Angeles, CA, United States: Springer. https://doi.org/10.1007/978-3-642-03237-0_3
Seghir, Mohamed, Andreas Podelski, and Thomas Wies. “Abstraction Refinement for Quantified Array Assertions.” In 16th International Symposium on Static Analysis, 5673:3–18. Springer, 2009. https://doi.org/10.1007/978-3-642-03237-0_3.
M. Seghir, A. Podelski, and T. Wies, “Abstraction refinement for quantified array assertions,” in 16th International Symposium on Static Analysis, Los Angeles, CA, United States, 2009, vol. 5673, pp. 3–18.
Seghir M, Podelski A, Wies T. 2009. Abstraction refinement for quantified array assertions. 16th International Symposium on Static Analysis. SAS: Static Analysis Symposium, LNCS, vol. 5673, 3–18.
Seghir, Mohamed, et al. “Abstraction Refinement for Quantified Array Assertions.” 16th International Symposium on Static Analysis, vol. 5673, Springer, 2009, pp. 3–18, doi:10.1007/978-3-642-03237-0_3.
Google Scholar