Improving Performance of the VerCors Program Verifier

Henk Mulder; Marieke Huisman; Sebastiaan Joosten

doi:10.1007/978-3-030-64354-6_3

Improving Performance of the VerCors Program Verifier

Henk Mulder, Marieke Huisman^*, Sebastiaan Joosten

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

54 Downloads (Pure)

Abstract

As program verification tools are becoming more powerful, and are used on larger programs, their performance also becomes more and more important. In this paper we investigate performance bottlenecks in the VerCors program verifier. Moreover, we also discuss two solutions to the identified performance bottlenecks: an improved encoding of arrays, as well as a technique to automatically generate trigger expressions to guide the underlying prover when reasoning about quantifiers. For both solutions we measure the effect on the performance. We see that the new encoding vastly reduces the verification time of certain programs, while other programs keep showing comparable times. This effect remains when moving to newer backends for VerCors.

Original language	English
Title of host publication	Deductive Software Verification: Future Perspectives
Subtitle of host publication	Reflections on the Occasion of 20 Years of KeY
Editors	Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Mattias Ulbrich
Place of Publication	Cham
Publisher	Springer
Pages	65-82
Number of pages	18
ISBN (Electronic)	978-3-030-64354-6
ISBN (Print)	978-3-030-64353-9
DOIs	https://doi.org/10.1007/978-3-030-64354-6_3
Publication status	Published - 4 Dec 2020

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	12345
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Keywords

22/2 OA procedure

Access to Document

10.1007/978-3-030-64354-6_3

ArticleFinal published version, 543 KBLicence: Taverne

Cite this

Mulder, H., Huisman, M., & Joosten, S. (2020). Improving Performance of the VerCors Program Verifier. In W. Ahrendt, B. Beckert, R. Bubel, R. Hähnle, & M. Ulbrich (Eds.), Deductive Software Verification: Future Perspectives: Reflections on the Occasion of 20 Years of KeY (pp. 65-82). (Lecture Notes in Computer Science; Vol. 12345). Springer. https://doi.org/10.1007/978-3-030-64354-6_3

Mulder, Henk ; Huisman, Marieke ; Joosten, Sebastiaan. / Improving Performance of the VerCors Program Verifier. Deductive Software Verification: Future Perspectives: Reflections on the Occasion of 20 Years of KeY. editor / Wolfgang Ahrendt ; Bernhard Beckert ; Richard Bubel ; Reiner Hähnle ; Mattias Ulbrich. Cham : Springer, 2020. pp. 65-82 (Lecture Notes in Computer Science).

@inbook{629eae67ae304c6e9e843bda7ea80ac1,

title = "Improving Performance of the VerCors Program Verifier",

abstract = "As program verification tools are becoming more powerful, and are used on larger programs, their performance also becomes more and more important. In this paper we investigate performance bottlenecks in the VerCors program verifier. Moreover, we also discuss two solutions to the identified performance bottlenecks: an improved encoding of arrays, as well as a technique to automatically generate trigger expressions to guide the underlying prover when reasoning about quantifiers. For both solutions we measure the effect on the performance. We see that the new encoding vastly reduces the verification time of certain programs, while other programs keep showing comparable times. This effect remains when moving to newer backends for VerCors.",

keywords = "22/2 OA procedure",

author = "Henk Mulder and Marieke Huisman and Sebastiaan Joosten",

year = "2020",

month = dec,

day = "4",

doi = "10.1007/978-3-030-64354-6_3",

language = "English",

isbn = "978-3-030-64353-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "65--82",

editor = "Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H{\"a}hnle and Mattias Ulbrich",

booktitle = "Deductive Software Verification: Future Perspectives",

address = "Germany",

}

Mulder, H, Huisman, M & Joosten, S 2020, Improving Performance of the VerCors Program Verifier. in W Ahrendt, B Beckert, R Bubel, R Hähnle & M Ulbrich (eds), Deductive Software Verification: Future Perspectives: Reflections on the Occasion of 20 Years of KeY. Lecture Notes in Computer Science, vol. 12345, Springer, Cham, pp. 65-82. https://doi.org/10.1007/978-3-030-64354-6_3

Improving Performance of the VerCors Program Verifier. / Mulder, Henk; Huisman, Marieke; Joosten, Sebastiaan.
Deductive Software Verification: Future Perspectives: Reflections on the Occasion of 20 Years of KeY. ed. / Wolfgang Ahrendt; Bernhard Beckert; Richard Bubel; Reiner Hähnle; Mattias Ulbrich. Cham: Springer, 2020. p. 65-82 (Lecture Notes in Computer Science; Vol. 12345).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

TY - CHAP

T1 - Improving Performance of the VerCors Program Verifier

AU - Mulder, Henk

AU - Huisman, Marieke

AU - Joosten, Sebastiaan

PY - 2020/12/4

Y1 - 2020/12/4

N2 - As program verification tools are becoming more powerful, and are used on larger programs, their performance also becomes more and more important. In this paper we investigate performance bottlenecks in the VerCors program verifier. Moreover, we also discuss two solutions to the identified performance bottlenecks: an improved encoding of arrays, as well as a technique to automatically generate trigger expressions to guide the underlying prover when reasoning about quantifiers. For both solutions we measure the effect on the performance. We see that the new encoding vastly reduces the verification time of certain programs, while other programs keep showing comparable times. This effect remains when moving to newer backends for VerCors.

AB - As program verification tools are becoming more powerful, and are used on larger programs, their performance also becomes more and more important. In this paper we investigate performance bottlenecks in the VerCors program verifier. Moreover, we also discuss two solutions to the identified performance bottlenecks: an improved encoding of arrays, as well as a technique to automatically generate trigger expressions to guide the underlying prover when reasoning about quantifiers. For both solutions we measure the effect on the performance. We see that the new encoding vastly reduces the verification time of certain programs, while other programs keep showing comparable times. This effect remains when moving to newer backends for VerCors.

KW - 22/2 OA procedure

U2 - 10.1007/978-3-030-64354-6_3

DO - 10.1007/978-3-030-64354-6_3

M3 - Chapter

SN - 978-3-030-64353-9

T3 - Lecture Notes in Computer Science

SP - 65

EP - 82

BT - Deductive Software Verification: Future Perspectives

A2 - Ahrendt, Wolfgang

A2 - Beckert, Bernhard

A2 - Bubel, Richard

A2 - Hähnle, Reiner

A2 - Ulbrich, Mattias

PB - Springer

CY - Cham

ER -

Improving Performance of the VerCors Program Verifier

Abstract

Publication series

Keywords

Access to Document

Fingerprint

Cite this