Lampropoulos Receives $540K NSF Award to Advance Proof Engineering Software and Protocols

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 $540K award. The funding comes from the NSF’s Division of Computing and Communication Foundations. 

Currently, the use of software with machine-checked proofs for correctness is reaching an unprecedented scale. Verified software is increasingly used in critical domains such as distributed systems and security, as well as in mainstream applications such as autonomous vehicles and web browsers. 
Lampropoulos says that the workflow for developing verified software using proof assistants is fundamentally different than techniques used for mainstream programming languages.

Design and development, he says, are driven by the requirements for formal specification and manageable burdens of proof, resulting in complex organization of components and in unorthodox processes and methodologies.

Moreover, despite over 40 years of development, proof assistants are not currently well adapted to large-scale software development and are expensive to use in terms of both time and expertise.
Lampropoulos and his team believe that research in traditional software engineering should be used as an inspiration to develop novel techniques to improve productivity in large-scale projects that use proof assistants, and to facilitate proliferation of formally verified software. 

“Over the years, we have identified—from our own proof efforts and our close interactions with proof engineers and proof assistant developers—a number of challenges that limit rapid progress of large verification projects,” says Lampropoulos, who is also a core faculty member in the Maryland Cybersecurity Center (MC2).
Lampropoulos is working on the NSF-funded project with Milos Gligoric, co-principal investigator on the grant and an assistant professor of electrical and computer engineering at the University of Texas at Austin, and 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.” 

—Story by Melissa Brachfeld