Deixis Online

Drones at work. Defense and other life-and-death applications are only as reliable as their software. (Photo: Air Force Staff Sgt. Rachel Simones.)

Computers are embedded in almost all aspects of daily life, including medical and defense applications where lives are at stake. Computer scientist Ariel Kellison of Cornell University works on methods to verify that such software works as it should.  The research allows the Department of Energy Computational Science Graduate Fellowship (DOE CSGF) recipient to blend her background in computational physics and love of mathematics with a desire to apply computing to important research problems at the national labs

Kellison has always enjoyed math and solving problems. As a high school student, she took accelerated math courses at a local community college and pursued her interest in astronomy. At the University of California, Santa Cruz, where she earned a bachelor’s degree in astrophysics, she dove into computer science, modeling magnetized fluids using hydrodynamics code.

Even before her Ph.D. studies, she worked with Cornell researchers on software verification. Her graduate work on high-performance computing (HPC) simulations are now informing some policy decisions. During the COVID-19 pandemic, for example, scenario modeling about the spread of the SARS-CoV-2 virus helped to guide the government response.

Kellison saw the opportunity to apply these tools, known as formal methods, to new challenges in verifying programs that rely on floating point computation, the basis of HPC. “It was clear that there was a need for advancing formal methods,” she says. “But it wasn’t totally clear how to bridge that gap at that time, and I found that pretty exciting.”

The DOE CSGF has allowed her to follow that path, working with David Bindel at Cornell and Andrew Appel at Princeton University. Academic researchers tend to emphasize theory over functional design, Kellison says. In one recent paper in the Proceedings of the 30^th IEEE International Symposium on Computer Arithmetic, they demonstrated one example of how to verify widely used linear algebra code.

However, “one of the things that’s really great about the CSGF is it pairs you with labs that are currently in need of tools that can be deployed,” she says. Kellison completed a 2021 practicum at Sandia National Laboratories in California and continues to work with the digital foundations and mathematics department as a year-round intern. “I get to hear about how formal methods are used in the lab and outside my wheelhouse, which is really cool.”

Applying those tools comes with a new set of challenges, she says, because they need to scale to realistic settings. “It’s possible, we’re working on it, but it is very time consuming — and requires a lot of collaboration,” she says. She’s also built a professional network with interns from other universities.

Outside work, Kellison spends time with her daughter and enjoys backpacking and baking. Kellison plans to defend her Ph.D. this fall and pursue a career with a national lab.