Making Proof Quest Effective for An Automated Prover

ABSTRACTThe goal of software verification is to establish the correctness of a program formally. Verification of programs that involve combinations of novel and sophisticated data abstractions is a challenge because their verification typically involves mathematical domains for which there are no decision procedures. This research leverages the existing RESOLVE verifying compiler. A central piece of such a compiler is its prover. To scale up, the prover needs to instantiate and utilize appropriate theorems from arbitrary mathematical theory units. This research aims to replace the existing prototype prover with a more powerful one suitable for proving verification conditions in sequent form. The new prover uses a three-tiered searching strategy to optimize the proof quest by eliminating the exploration of unnecessary search spaces. The research uses generic maps and trees to experiment with the proposed strategy and evaluate the new prover.