Program verification using dynamic invariants and theorem prover: Exploratory study on Daikon and SAW
Date
2023-08
Authors
Pal, Sanchayani
Major Professor
Advisor
Basu, Samik
Cohen, Myra
Tian, Jin
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Authors
Research Projects
Organizational Units
Journal Issue
Is Version Of
Versions
Series
Department
Computer Science
Abstract
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.