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

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

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 $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.”

Original story written by Melissa Brachfeld

June 30, 2021


Prev   Next



Current Headlines

UMD Leads New $25M NSF Quantum Leap Challenge Institute for Robust Quantum Simulation

Michael Fu Works to Improve Kidney Transplants With NSF Grant

IonQ Joins University of Maryland Quantum Startup Foundry, Receives National Innovation Award

Entomology and Extension Faculty Join a National Team to Study and Support Diverse Perennial Forage Systems with Major Implications for Human and Animal Ecosystem Health

Sangeetha Madhavan Publishes New Research On Families’ Economic Inequalities In Sub-Saharan Africa

Technology for All

Center for Substance Abuse Research Receives Funding to Expand the Emergency Department Drug Surveillance System Nationwide

Student Journalism Project Sheds Light on Role of White Supremacist Newspapers in Fueling Racial Tension, Violence

News Resources

Return to Newsroom

Search News

Archived News

Events Resources

Events Calendar

Additional Resources

UM Newsdesk

Faculty Experts

Connect

social iconstwitterlinkedinrssYouTube
Division of Research
University of Maryland
College Park, MD 20742-1541
© Copyright 2021 University of Maryland

Did You Know

Kevin Plank, co-founder of Under Armour, is an alumnus of the University of Maryland.