Speaker:Sanchayani Pal

Automatically Verify Algorithms Using Invariants

Program verification can be immensely important in code development, minimizing and/or eliminating bugs, code maintenance, reusability of code and so on. While there can be several ways of verifying a program, having a program verified automatically can be highly efficient in terms of reducing time and manual effort. In this study, our objective is to build a verification technique that provides an end-to-end solution which can be used to verify certain properties for a category of C programs. We present an automated approach of generating mathematical specification for a given program from the set of invariants produced by an invariant detector tool followed by proving the validity of the identified invariants using formal proofs, thereby, verifying a property of a given program.

Committee: Samik Basu (co-major professor), Myra Cohen (co-major professor), and Jin Tian

Join on Zoom: https://iastate.zoom.us/j/93859637637