Program verification using dynamic invariants and theorem prover: Exploratory study on Daikon and SAW
Basu, Samik Cohen, Myra Tian, Jin
Is Version Of
Program verification, in general, is undecidable. In the recent years, SMT/SAT solver based proof assistants and theorem provers have been deployed to prove desirable (e.g., necessary pre-/post-conditions of functions) properties of programs in a semi-automatic fashion relying on some expert knowledge and guidance. In this context, we investigate the viability of Software Analysis Workbench (SAW) infrastructure and Daikon invariant detector tool in verifying properties of programs. Our main objective is to deploy Daikon to generate relevant invariants of programs automatically, and then utilize those invariants to develop functional specifications of programs. We conjecture that such specifications can be automatically translated into executable languages (such as Cryptol) and can be effectively utilized to prove desired properties of programs. This is likely to minimize expert knowledge necessary to develop program specifications, thus improving the applicability of proof assistants and theorem provers in effectively checking the properties of programs.