Extending VIAP to Handle Array Programs

Pritom Rajkhowa; Fangzhen Lin

doi:10.1007/978-3-030-03592-1_3

Extending VIAP to Handle Array Programs

Pritom Rajkhowa^*, Fangzhen Lin

^*Corresponding author for this work

Department of Computer Science and Engineering

Research output: Chapter in Book/Conference Proceeding/Report › Conference Paper published in a book › peer-review

8 Citations (Scopus)

Abstract

In this paper, we extend our previously described fully automated program verification system called VIAP primarily for verifying the safety properties of programs with integer assignments to programs with arrays. VIAP is based on a recent translation of programs to first-order logic proposed by Lin [1] and directly calls the SMT solver Z3. It relies more on reasoning with recurrences instead of loop invariants. In this paper, we extend it to programs with arrays. Our extension is not restricted to single dimensional arrays but general and works for multidimensional and nested arrays as well. In the most recent SV-COMP 2018 competition, VIAP with array extension came in second in the ReachSafety-Arrays sub-category, behind VeriAbs.

Original language	English
Title of host publication	Verified Software. Theories, Tools, and Experiments - 10th International Conference, VSTTE 2018, Revised Selected Papers
Editors	Ruzica Piskac, Philipp Rümmer
Publisher	Springer Verlag
Pages	38-49
Number of pages	12
ISBN (Print)	9783030035914
DOIs	https://doi.org/10.1007/978-3-030-03592-1_3
Publication status	Published - 2018
Event	10th International Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2018 - Oxford, United Kingdom Duration: 18 Jul 2018 → 19 Jul 2018

Publication series

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

Conference

Conference	10th International Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2018
Country/Territory	United Kingdom
City	Oxford
Period	18/07/18 → 19/07/18

Bibliographical note

Publisher Copyright:
© 2018, Springer Nature Switzerland AG.

Keywords

Arithmetic
Array
Automatic program verification
First-order logic
Mathematical induction
Multi-dimensional
Nested
Recurrences
SMT
Structure

Access to Document

10.1007/978-3-030-03592-1_3

Cite this

Rajkhowa, P., & Lin, F. (2018). Extending VIAP to Handle Array Programs. In R. Piskac, & P. Rümmer (Eds.), Verified Software. Theories, Tools, and Experiments - 10th International Conference, VSTTE 2018, Revised Selected Papers (pp. 38-49). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11294 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-030-03592-1_3

Rajkhowa, Pritom ; Lin, Fangzhen. / Extending VIAP to Handle Array Programs. Verified Software. Theories, Tools, and Experiments - 10th International Conference, VSTTE 2018, Revised Selected Papers. editor / Ruzica Piskac ; Philipp Rümmer. Springer Verlag, 2018. pp. 38-49 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{87290f8334254456a06be37132f22f22,

title = "Extending VIAP to Handle Array Programs",

abstract = "In this paper, we extend our previously described fully automated program verification system called VIAP primarily for verifying the safety properties of programs with integer assignments to programs with arrays. VIAP is based on a recent translation of programs to first-order logic proposed by Lin [1] and directly calls the SMT solver Z3. It relies more on reasoning with recurrences instead of loop invariants. In this paper, we extend it to programs with arrays. Our extension is not restricted to single dimensional arrays but general and works for multidimensional and nested arrays as well. In the most recent SV-COMP 2018 competition, VIAP with array extension came in second in the ReachSafety-Arrays sub-category, behind VeriAbs.",

keywords = "Arithmetic, Array, Automatic program verification, First-order logic, Mathematical induction, Multi-dimensional, Nested, Recurrences, SMT, Structure",

author = "Pritom Rajkhowa and Fangzhen Lin",

note = "Publisher Copyright: {\textcopyright} 2018, Springer Nature Switzerland AG.; 10th International Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2018 ; Conference date: 18-07-2018 Through 19-07-2018",

year = "2018",

doi = "10.1007/978-3-030-03592-1\_3",

language = "English",

isbn = "9783030035914",

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

publisher = "Springer Verlag",

pages = "38--49",

editor = "Ruzica Piskac and Philipp R{\"u}mmer",

booktitle = "Verified Software. Theories, Tools, and Experiments - 10th International Conference, VSTTE 2018, Revised Selected Papers",

}

Rajkhowa, P & Lin, F 2018, Extending VIAP to Handle Array Programs. in R Piskac & P Rümmer (eds), Verified Software. Theories, Tools, and Experiments - 10th International Conference, VSTTE 2018, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11294 LNCS, Springer Verlag, pp. 38-49, 10th International Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2018, Oxford, United Kingdom, 18/07/18. https://doi.org/10.1007/978-3-030-03592-1_3

Extending VIAP to Handle Array Programs. / Rajkhowa, Pritom; Lin, Fangzhen.
Verified Software. Theories, Tools, and Experiments - 10th International Conference, VSTTE 2018, Revised Selected Papers. ed. / Ruzica Piskac; Philipp Rümmer. Springer Verlag, 2018. p. 38-49 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11294 LNCS).

Research output: Chapter in Book/Conference Proceeding/Report › Conference Paper published in a book › peer-review

TY - GEN

T1 - Extending VIAP to Handle Array Programs

AU - Rajkhowa, Pritom

AU - Lin, Fangzhen

PY - 2018

Y1 - 2018

N2 - In this paper, we extend our previously described fully automated program verification system called VIAP primarily for verifying the safety properties of programs with integer assignments to programs with arrays. VIAP is based on a recent translation of programs to first-order logic proposed by Lin [1] and directly calls the SMT solver Z3. It relies more on reasoning with recurrences instead of loop invariants. In this paper, we extend it to programs with arrays. Our extension is not restricted to single dimensional arrays but general and works for multidimensional and nested arrays as well. In the most recent SV-COMP 2018 competition, VIAP with array extension came in second in the ReachSafety-Arrays sub-category, behind VeriAbs.

AB - In this paper, we extend our previously described fully automated program verification system called VIAP primarily for verifying the safety properties of programs with integer assignments to programs with arrays. VIAP is based on a recent translation of programs to first-order logic proposed by Lin [1] and directly calls the SMT solver Z3. It relies more on reasoning with recurrences instead of loop invariants. In this paper, we extend it to programs with arrays. Our extension is not restricted to single dimensional arrays but general and works for multidimensional and nested arrays as well. In the most recent SV-COMP 2018 competition, VIAP with array extension came in second in the ReachSafety-Arrays sub-category, behind VeriAbs.

KW - Arithmetic

KW - Array

KW - Automatic program verification

KW - First-order logic

KW - Mathematical induction

KW - Multi-dimensional

KW - Nested

KW - Recurrences

KW - SMT

KW - Structure

UR - https://www.webofscience.com/wos/woscc/full-record/WOS:000674473500003

UR - https://openalex.org/W2887225054

UR - https://www.scopus.com/pages/publications/85057408882

U2 - 10.1007/978-3-030-03592-1_3

DO - 10.1007/978-3-030-03592-1_3

M3 - Conference Paper published in a book

SN - 9783030035914

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 38

EP - 49

BT - Verified Software. Theories, Tools, and Experiments - 10th International Conference, VSTTE 2018, Revised Selected Papers

A2 - Piskac, Ruzica

A2 - Rümmer, Philipp

PB - Springer Verlag

T2 - 10th International Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2018

Y2 - 18 July 2018 through 19 July 2018

ER -

Rajkhowa P, Lin F. Extending VIAP to Handle Array Programs. In Piskac R, Rümmer P, editors, Verified Software. Theories, Tools, and Experiments - 10th International Conference, VSTTE 2018, Revised Selected Papers. Springer Verlag. 2018. p. 38-49. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-03592-1_3

Extending VIAP to Handle Array Programs

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this