A University of Maryland expert in programming languages has received a National Science Foundation (NSF) award to advance the development and maintenance of large and evolving software verification projects that use proof assistants.
Proof assistants are software tools to assist in proofs—formal verification—of complex mathematical equations used in computing.
Leonidas Lampropoulos, an assistant professor of computer science with an appointment in the University of Maryland Institute for Advanced Computer Studies (UMIACS), is co-principal investigator of the Maryland Cybersecurity Center (MC2).
Lampropoulos is working on the NSF-funded project with Henry Blanchette, a first-year UMD computer science doctoral student.
“Ideally, building verified software and working with proof assistants should be much easier and much more scalable compared to where we are now. The community has already made great strides in reducing the barrier to entry,” Lampropoulos says. “Still, anyone who has used any proof assistant in a serious capacity is probably in a position to voice multiple frustrations. Milos and I are no exception, so when Milos approached me last year to do something about it, I jumped at the opportunity.”
Original story written by Melissa Brachfeld