TY - GEN
T1 - Abstraction refinement for quantified array assertions
AU - Seghir, Mohamed Nassim
AU - Podelski, Andreas
AU - Wies, Thomas
PY - 2009
Y1 - 2009
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=70350343345&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=70350343345&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-03237-0_3
DO - 10.1007/978-3-642-03237-0_3
M3 - Conference contribution
AN - SCOPUS:70350343345
SN - 3642032362
SN - 9783642032363
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 3
EP - 18
BT - Static Analysis - 16th International Symposium, SAS 2009, Proceedings
T2 - 16th International Symposium on Static Analysis, SAS 2009
Y2 - 9 August 2009 through 11 August 2009
ER -