Formal Methods at Khoury College of Computer Sciences
Advancing scientifically rigorous approaches to assessing and verifying software
Khoury College research in formal methods taps the science of software by developing formal proofs to determine what predictions can be made about the program programs we write. For example, how can we be certain that a program will give correct results, that it will always terminate, or that it will not throw an exception, causing an error? Creating the foundation for this knowledge is the heart of formal methods.
Researchers use formal proofs and other rigorous logical and mathematical techniques to verify that programs are correct, not just in a single instance, but in all possible cases under which it might be used. Complementing other modes of software testing, formal methods research reveals a more complete view of vulnerabilities.
Because formal methods research brings together practices from mathematics and science, among other fields, it sheds light on the foundations and limits of computer programming and can help expand those limits.
Ensuring the safety and reliability of systems
Research on formal methods is key to making sure that the software underlying so much of modern life is correct, secure, reliable, and as free of bias as possible. Given that software is firmly at the heart of many safety-critical systems — for instance, how planes navigate or medical technology delivers life-saving treatments — the software has to be as rigorously tested as any other aspect of the system.
But ensuring the validity of software in these systems is a formidable task, and formal methods is a key part of the solution. It provides the means to assess and verify not just a single case, but all the cases for a program — critical knowledge for making the world’s computer systems and networks work correctly.
Sample research areas
- Synthesis of distributed protocols
- Inductive invariant inference
- Verification of neural-network controlled systems
- Shield synthesis for reinforcement learning
- Equivalence checking for neural networks
- Refinement
- Compositionality
- Validity
Domains of interest
- Computer science
- Formal methods
- Formal specification and verification
- Program synthesis
- Logic
- Computer-aided reasoning
- Theorem proving
- Embedded and cyber-physical systems
- Security
- Trustworthy AI
- Theoretical computer science
Current project highlights
Safe Multi-Agent Reinforcement Learning with Shielding
Reinforcement learning (RL) approaches are used in many computer systems with multiple agents, such as those that guide robot or auto navigation. But how can these approaches be validated as correct, essential in safety-critical settings? Formal methods research can be applied, and Khoury researchers are addressing how to use these techniques at scale.
SaTC: CORE: Medium: Collaborative: Bridging the Gap between Protocol Design and Implementation through Automated Mapping
Computer networks and internet connectivity are essential, yet the protocols at the heart of networks are plagued by security problems. Formal Methods faculty at Khoury College are developing new methodologies and models for protocol design and implementation with the promise to automate verification and make networks more secure.
Recent research publications
A Nominal Approach to Probabilistic Separation Logic
Authors: John M. Li, Jon Aytac, Philip Johnson-Freyd, Amal Ahmed, Steven Holtzen
Khoury College researchers have made a breakthrough in computer science by connecting two different ways of understanding how uncertain events unfold in computer systems. This research bridges a gap between the mathematical tools used by probability experts and those used by computer scientists to formally reason about programs. By showing that these two approaches are essentially the same, researchers have laid the groundwork for more robust and reliable software systems.
Efficient Synthesis of Symbolic Distributed Protocols by Sketching
Authors: Derek Egolf, William Schultz, Stavros Tripakis
Researchers have developed a new tool, SCYTHE, to automatically create complex computer programs that control multiple systems. This tool can design protocols, such as those used to manage distributed systems, by starting with a basic outline and then filling in the details. SCYTHE is faster than previous methods and can handle much larger and more complex problems. This research has the potential to improve how we build and maintain complex software systems.
Probabilistic Logic Programming Semantics for Procedural Content Generation
Authors: Abdelrahman Madkour, Chris Martens, Steven Holtzen, Casper Harteveld, Stacy Marsella
Khoury College researchers have developed a new method for creating game content automatically. This work combines machine learning approaches and traditional programming but gives developers more control over the generated content. By using probabilistic logic, developers can specify the desired characteristics of the content, such as the size of a maze or the difficulty of a puzzle, while also allowing the computer to generate different possibilities. This approach enlarges the capacity of game developers to create varied and creative game worlds.
Related labs and groups
Faculty members
-
Gene Cooperman
Gene Cooperman is a professor at Khoury College and leader of the High Performance Computing Laboratory. He researches a slew of interdisciplinary computing, math, and physics topics, and contributed to “GEANT4 – A Simulation Toolkit” — the most widely cited paper in high-energy physics.
-
Joshua Gancher
Joshua Gancher is an assistant professor at Khoury College. His research into cryptographic software and formal methods seeks to mathematically verify the security of foundational software, and to create tools to do that process at scale.
-
Steve Holtzen
Steve Holtzen is an assistant professor at Khoury College, affiliated with the Programming Research Laboratory. His research aims to design fast, accessible, and useful probabilistic modeling systems for everyday reasoning tasks, and he teaches courses on artificial intelligence, programming languages, and machine learning.
-
Panagiotis (Pete) Manolios
Pete Manolios is a professor at Khoury College and the leader of the computer-aided reasoning group. His research uses formal methods to further the design, analysis, and implementation of aerospace, hardware, and component-based software systems.
-
Ji-Yong Shin
Ji-Yong Shin is an assistant professor at Khoury College. His research focuses on formal verification methods that can be applied to system designs, with additional interests in distributed systems, cloud storage systems, and operating systems.
-
Stavros Tripakis
Stavros Tripakis is an associate professor at Khoury College. His research centers on formal methods, computer-aided verification and synthesis, security, and safety-critical, embedded, and cyber-physical systems.