The National Science Foundation (NSF) has awarded Alexandra Silva, professor of computer science in the Cornell Ann S. Bowers College of Computing and Information Science, two $900,000 grants for projects related to verification of networks and software that exploits concurrency and randomness.
Generally, Silva's research focuses on semantics of programming languages and the use of algebraic methods in network verification.
"These two grants will enable needed foundational research to push the field of formal verification further and make the techniques more widely available in different application domains," Silva said. "I am excited to work on these projects with my close collaborators and students!"
The first grant comes via NSF’s Formal Methods in the Field Program. Along with Nate Foster, professor of computer science, Silva will explore automata learning – a technique for automatically inferring models of a system, even complex ones, by observing its inputs and outputs – with applications to yield more stable computer networks.
When computer networks go down, the outages can cause major disruptions for users. There are tools for verifying networked behavior that can catch bugs and make them more reliable, but these tools require precise models of the devices and connections in the systems being verified.
Silva and Foster's work will develop new techniques that enable automatic construction of these models, so that people can more widely use formal verification – a method for ensuring that software is behaving correctly – to ensure the networks are working as desired.
The second NSF grant, with collaborator Joe Tassarotti, assistant professor of computer science at New York University, will support work to improve the reliability of software that makes use of randomness, which is commonly used for cryptography and machine learning.
They plan to develop new techniques for reasoning about randomness and concurrency in programs, which existing formal verification techniques for software debugging cannot handle. These techniques have the potential to improve software quality and prevent costly bugs. Silva said the research proposed in this grant was enabled by recent work led by Noam Zilberstein, a Ph.D. candidate in the field of computer science, which provided new techniques for more expressive program logics.