Title:
Formal reasoning about programs and programming languages

Abstract:
It is well known that it is important to ensure that programs, especially in critical applications, e.g., online banking, are correct. This is because program bugs can lead to issues including privacy violations and security vulnerabilities. There are different approaches to make sure that programs are correct. In this talk I will present my research on formal verification of programs and programming languages using program logics. A program logic is a formal framework that allows the user to reason about programs at a high level of abstraction. They allow the user to specify properties of programs and facilitate constructing formal and rigorous proofs of these specifications.

Join on Zoom Friday April 9th at 2PM