Skip to Main Content
 

Global Search Box

 
 
 
 

Files

File List


z3-mve.pdf (1.07 MB)

ETD Abstract Container

Abstract Header

Implementing a Resolve Online Prover Using Z3

Bentley, John
http://orcid.org/0000-0001-8685-790X
http://rave.ohiolink.edu/etdc/view?acc_num=osu1638207940230375

Abstract Details

2021, Master of Science, Ohio State University, Computer Science and Engineering.
The Resolve Online development environment currently supports multiple provers: Dafny, SplitDecision, and variations and combinations thereof. The existing provers used by Resolve Online have some areas of improvement. One downside of the Dafny prover is that it generates Dafny programs to discharge verification conditions, tying it closely to the specific version of the Dafny compiler used. This approach is brittle because new releases of Dafny tend to break the backend prover, making it difficult for the Resolve Online tool to leverage improvements in the Dafny language. Other areas of potential improvement include the number of verification conditions that are automatically discharged and the execution time of the provers. Z3 is a modern theorem prover developed at Microsoft Research. First released in 2012, Z3 is under active development, with 3 releases in the last year at the time of writing and frequent commits. Z3 is used by Boogie, F*, Pex, and more, as well as tools that indirectly use Z3 through Boogie. This ongoing development could lead to future improvements that will allow for better verification of Resolve programs in the future. In order to leverage Z3 in Resolve Online, we have extended Resolve Online by creating a new prover backend that uses Z3. A benchmark of Resolve code consisting of 30 examples was used. Each example was run with the three provers: the new Z3 backend, Dafny, and SplitDecision. In all examples Z3 is able to prove at least as many VCs as Dafny, and in 28 examples, Z3 was able to prove at least as many VCs as SplitDecision. There are 20 examples where Z3 proved more VCs than Dafny and 11 when compared to SplitDecision. A smaller benchmark consisting of 8 complex examples from the full benchmark was selected to be used for analyzing the execution time of the provers. In most cases, Dafny takes substantially longer than SplitDecision and Z3. SplitDecision and Z3 are both close in the execution times. Either one of the two could be faster depending on the example. However, there is one major outlier where Z3 is significantly faster than SplitDecision, running for under a minute while SplitDecition runs for around 3 hours.
Neelam Soundarajan (Committee Member)
Paolo Sivilotti (Advisor)
106 p.
Computer Science
z3 prover resolve verification smt

Recommended Citations

Citations

  • Bentley, J. (2021). Implementing a Resolve Online Prover Using Z3 [Master's thesis, Ohio State University]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=osu1638207940230375

    APA Style (7th edition)

  • Bentley, John. Implementing a Resolve Online Prover Using Z3. 2021. Ohio State University, Master's thesis. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=osu1638207940230375.

    MLA Style (8th edition)

  • Bentley, John. "Implementing a Resolve Online Prover Using Z3." Master's thesis, Ohio State University, 2021. http://rave.ohiolink.edu/etdc/view?acc_num=osu1638207940230375

    Chicago Manual of Style (17th edition)

osu1638207940230375
492
© 2021, all rights reserved.
This open access ETD is published by The Ohio State University and OhioLINK.