W&M Homepage

This calendar presented by William & Mary

[PAST EVENT] Colloquium Talk: Verification for working developers

January 20, 2022
9am - 10am
Location
McGlothlin-Street Hall, Online on Zoom
251 Jamestown Rd
Williamsburg, VA 23185Map this location
Access & Features
  • Open to the public

Abstract:

In this talk I’ll discuss my research on practical verification for real software developers. The main technical topic will be my work on accumulation typestate automata, a special-case of traditional typestate automata that can be soundly checked without the need to run an expensive, whole-program alias analysis - making these “accumulation analyses” fast enough to run every time that software is compiled. I’ll cover both the theory and its practical applications to two real-world problems: that programs initialize objects correctly and that programs are free of resource leaks. I’ll also briefly discuss some of my other work applying verification tools to compliance problems in industry and future research directions.


Short Bio:

Martin Kellogg is finishing up his PhD at the University of Washington in the PLSE group, advised by Mike Ernst. His work is focused on making verification practical for real software engineers. He has published in top-tier Software Engineering venues including ICSE, ESEC/FSE, and ASE. He collaborates extensively with industry, especially with the AWS Automated Reasoning Group.

Contact

Weizhen Mao