CySER Virtual Seminar – Correctness and Verification using Software Contracts

About the event

Title: Correctness and Verification using Software Contracts

Speaker: Thomas Gilray

Abstract: Software systems are among the most complex human-engineered artifacts, often spanning multiple languages and layers of abstraction, as well as many thousands of lines of code. In light of this evolving complexity, what does it mean for code to be correct and how can we audit or even formally verify its correctness? In this talk, I will introduce the idea of software contracts as an approach to this problem and discuss some of my own research on automating program analysis from this point of view. Contracts give us a powerful language-based approach to declarative specification of program properties relevant to correctness, including security and privacy, and both a method for dynamically monitoring and enforcing those properties, as well as scaffolding that can guide piecemeal approaches to ahead-of-time verification.

Speaker Bio: Thomas Gilray is a new Associate Professor in the EECS department at Washington State University. He was previously Assistant Professor at the University of Alabama at Birmingham and Victor Basili Fellow at the University of Maryland, College Park. His research focuses on designing and implementing tunable, general-purpose systems for reasoning about software at scale, leveraging techniques from programming languages, formal methods, and highperformance computing to address applications in program understanding, verification, auditing, and optimization. Gilray’s research is currently being supported by grants from the NSF PPoSS program, DARPA V-SPELLS, and ARPA-H.

Learn more about CySER: https://cyser.wsu.edu/