Purdue ECE undergraduate Craig Liu

Purdue University undergraduate Craig Liu has been recognized nationally and internationally for his research on improving the way we verify computer programs.

Liu, a student in the Elmore Family School of Electrical and Computer Engineering, won first place in the undergraduate category of the Student Research Competition (SRC) at SPLASH 2024, one of the premier conferences in programming languages and software engineering. His winning research, titled “Design of Fractional Permissions for a Gradual Verifier,” tackles a long-standing challenge in software verification—ensuring program correctness while reducing the burden on developers.

Following his win at SPLASH, Liu advanced to the prestigious ACM Student Research Competition Grand Finals, where he earned second place in the undergraduate category. The Grand Finals, hosted by the Association for Computing Machinery (ACM), bring together top student researchers from computing conferences around the world.

"It was a great opportunity to present my research at the SRC and I'm honored to receive these awards,” said Liu. “I worked on making gradual verification more amenable to the verification of concurrent programs - programs where multiple computations are executed during the same time period. Such programs are widely used in software, with one example being several users simultaneously browsing a website. I am very grateful to Professor DiVincenzo for her invaluable mentorship and support."

Liu’s project addresses a key limitation in a tool called Gradual C0, which helps verify whether software programs behave as intended. Traditional static verification tools require developers to manually write extremely detailed annotations to prove that their programs are correct—an often time-consuming and error-prone process. Gradual verification simplifies this by allowing partial specifications, relying on both static checks and dynamic (run-time) checks when needed.

Gradual C0 already supports basic permission checks for accessing parts of a program's memory. However, until now, it could only handle situations where a program either had full access to memory or none at all. Liu’s research adds fractional permissions to the mix—a sophisticated way to represent partial access. This is especially important for programs that run concurrent processes, where, for example, one part of a program might read data while another writes to it.

Fractional permissions let developers precisely describe different levels of access. A fraction less than 1 allows read access, while a full value of 1 is needed for writing. Liu extended the Gradual C0 verifier to support this nuance, enabling more powerful and flexible program verification.

Jenna DiVincenzo, assistant professor of electrical and computer engineering, said gradual verification allows developers to apply formal verification techniques more flexibly rather than in an all-or-nothing fashion.

“Developers can specify and verify critical software components, like collision avoidance systems, with heavy-weight techniques that provide strong correctness guarantees and apply light-weight techniques in less critical components,” said DiVincenzo. “Craig made crucial advancements in gradual verification technology, which allows it to be used on more classes of software and with specification generation techniques.”

By introducing these capabilities, Liu’s work lays the foundation for better tools to write safer and more reliable software—especially for systems where concurrency and memory access must be carefully controlled. His project was selected from among numerous undergraduate research efforts from across the globe, demonstrating not only technical innovation but also potential real-world impact.