Program verification using dynamic invariants and theorem prover: Exploratory study on Daikon and SAW

Thumbnail Image
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.
Comments
Description
Keywords
Citation
DOI
Source
Subject Categories
Copyright