Mar 9
CS Tea Talk with Will Leeson: "Do what I want, not what I say: Proving software acts according to plan"
Abstract:
Software touches many aspects of the world as we know it. More and more, safety critical systems, such as medical devices and autonomous systems, rely on software to behave to specification. For example, a specification for the software controlling an elevator could be "If the cabin is in motion, the doors should never open". Systems can be thoroughly tested to discover bugs, but to prove the system does not violate its specifications, we must turn to software verification. Software verification is a technique which seeks to prove that a piece of software meets some specification of "correctness". There are many software verification techniques, and it can be difficult to know which will be the most effective for an expert in verification, let alone a non-expert software developer. In this talk, I will describe how we can define "correctness", give an overview of several core techniques in software verification, and describe a technique for automatically selecting a software verification tool given a program and specification.
Will Leeson is a Ph.D. candidate in the Department of Computer Science at the University of Virginia. His research is focused on improving software engineering tools by replacing human-designed heuristics with machine learning models which leverage rich graph representations. His work has been published at TACAS and is to appear at ICSE 2023. He has been awarded the Outstanding Teaching Award for his teaching in the Department of Computer Science at the University of Virginia.
from Computer Science