Techniques to Improve Automated Software Verification

Formally specifying a program and verifying its implementation against the specification allows one to prove its correctness. This process involves writing an accurate specification, generating verification conditions (VCs) from the annotated implementation and then successfully proving the VCs to be correct. Correctness of the VCs implies correctness of the program.;The entire process of verifying an implementation against its specification assumes that the specification is correct in the first place. Therefore we take a step back and describe some rules to perform sanity checks on the specification to ensure that it is consistent. We also develop techniques to detect errors in program annotations.;Recent developments in automated theorem proving tools have ensured that minimum user interaction is needed to ascertain the validity of most VCs. While this appears to reduce the burden on the software engineers, in the case a VC cannot be proved automatically the user cannot interactively "guide" the prover. This impediment is especially noticed while verifying VCs generated from programs whose specifications involve quantifiers, since automated theorem provers often fail to prove them. To overcome this difficulty, we seek to incrementally improve the overall effectiveness of automated theorem provers by helping them prove VCs involving user-defined mathematical functions and predicates involving quantifiers. We do this by supplying universal algebraic lemmas about these functions as an alternative to expanding their definitions.;We also describe a lightweight, semi-automated method to add a catalogue of correct universal algebraic lemmas corresponding to a user-defined function. These lemmas are at first generated from pre-defined templates, and then a mathematician is responsible for selecting the correct ones in an interactive manner.