Primariliy engaged in theoretical research in the past, members of this research group are now using formal methods to transform the design and implementation of highly reliable, robust and scalable systems in important application domains such as cyber security, aerospace systemss, computational biology and public health. Their work includes collaborations with NASA and Boeing to design formal verification tools that help achieve the highest level of systems reliability.
Members of the Formal Methods research group are involved with the formal verification and validation of large-scale computing systems as well as model checking concurrent software and multithread programs. Researchers also conduct formal modeling of obfuscation techniques to defend against malicious attacks, examining the limits of this security approach.
Team Achievements
- Developed ACL2 sedan, a modified version of ACL2 (A Computational Logic for Applicative Common Lisp) that enables students and other novices to reason about programs
- Developed a method to synthesize architectural models of systems that interact with the physical world in real time and benefit aerospace industry design at the earliest stages, when time, cost and overall system efficiency can benefit most
- Contributing to the formal methods aspects of a DARPA (Defense Against Research Projects Agency) effort to design new computer systems highly resistant to cyber attacks
- Developed hardware verification technology to verify bottlenecks in the design of a microprocessor and reason about hardware;
- Proposed an approach to modeling secrecy in multi-agent systems by defining a set of possible observations and providing agents with algorithms used to distinguish the possible states of the system.
