As our society grows increasingly reliant on computer systems, even the simplest of software errors can have devastating financial or security consequences. How can we find errors in real-world systems? How can we guarantee that such errors don't exist? To even begin to answer these questions we need a specification: a description of what it means for a piece of code to be correct.
In this talk, I will discuss my work on reasoning about software and specifications, focusing primarily on two techniques and their interplay: property-based testing and mechanized formal verification. Testing can quickly uncover errors in complex software, but it cannot guarantee their absence. Formal verification provides strong correctness guarantees, but is still very expensive in time and effort. Together, they are a match made in heaven.
Leonidas Lampropoulos is an assistant professor of Computer Science at the University of Maryland, College Park and a co-director of the PLUM lab. Before that, he was a Victor Basili postdoctoral fellow jointly between UMD and UPenn, under the supervision of Michael Hicks and Benjamin Pierce. He got his Ph.D. at the University of Pennsylvania. His research interests lie in programming languages, with an emphasis on software correctness through both random testing and verification. He is the principal author of the fourth volume in the popular Software Foundations series of online textbooks: "QuickChick: Property-Based Testing in Coq".