Abstraction refinement for quantified array assertions

Mohamed Nassim Seghir; Andreas Podelski; Thomas Wies

doi:10.1007/978-3-642-03237-0_3

Abstraction refinement for quantified array assertions

Mohamed Nassim Seghir, Andreas Podelski, Thomas Wies

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Static Analysis - 16th International Symposium, SAS 2009, Proceedings
Pages	3-18
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-03237-0_3
State	Published - 2009
Event	16th International Symposium on Static Analysis, SAS 2009 - Los Angeles, CA, United States Duration: Aug 9 2009 → Aug 11 2009

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	5673 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	16th International Symposium on Static Analysis, SAS 2009
Country/Territory	United States
City	Los Angeles, CA
Period	8/9/09 → 8/11/09

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-642-03237-0_3

Cite this

Seghir, M. N., Podelski, A., & Wies, T. (2009). Abstraction refinement for quantified array assertions. In Static Analysis - 16th International Symposium, SAS 2009, Proceedings (pp. 3-18). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5673 LNCS). https://doi.org/10.1007/978-3-642-03237-0_3

Abstraction refinement for quantified array assertions. / Seghir, Mohamed Nassim; Podelski, Andreas; Wies, Thomas.
Static Analysis - 16th International Symposium, SAS 2009, Proceedings. 2009. p. 3-18 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5673 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Seghir, MN, Podelski, A & Wies, T 2009, Abstraction refinement for quantified array assertions. in Static Analysis - 16th International Symposium, SAS 2009, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5673 LNCS, pp. 3-18, 16th International Symposium on Static Analysis, SAS 2009, Los Angeles, CA, United States, 8/9/09. https://doi.org/10.1007/978-3-642-03237-0_3

@inproceedings{4505e2203d7c4ba998e62dceacced11d,

title = "Abstraction refinement for quantified array assertions",

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.",

author = "Seghir, {Mohamed Nassim} and Andreas Podelski and Thomas Wies",

year = "2009",

doi = "10.1007/978-3-642-03237-0_3",

language = "English (US)",

isbn = "3642032362",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "3--18",

booktitle = "Static Analysis - 16th International Symposium, SAS 2009, Proceedings",

note = "16th International Symposium on Static Analysis, SAS 2009 ; Conference date: 09-08-2009 Through 11-08-2009",

}

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 -

Abstraction refinement for quantified array assertions

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this