BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Events//NONSGML v1.0//EN
METHOD:PUBLISH
BEGIN:VEVENT
DTSTART;TZID="Pacific Time (US & Canada)":20241001T121000
DTEND;TZID="Pacific Time (US & Canada)":20241001T130000
SUMMARY:CySER Virtual Seminar &#8211; Correctness and Verification using Software Contracts
LOCATION:Online
DESCRIPTION:Title: Correctness and Verification using Software Contracts\n\nSpeaker: Thomas Gilray\n\nAbstract: 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.\n\nSpeaker 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&#039;s research is currently being supported by grants from the NSF PPoSS program, DARPA V-SPELLS, and ARPA-H.\n\n&nbsp;\n\nLearn more about CySER: https://cyser.wsu.edu/
BEGIN:VALARM
ACTION:DISPLAY
DESCRIPTION:REMINDER
TRIGGER;RELATED=START:-PT00H15M00S
END:VALARM
END:VEVENT
END:VCALENDAR
