Master of Science, The Ohio State University, 2021, 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 on (open full item for complete abstract)

Committee: Neelam Soundarajan (Committee Member); Paolo Sivilotti (Advisor) Subjects: Computer Science