Research
Research Groups > Formal Methods
Panagiotis Manolios Panagiotis Manolios Thomas Wahl Thomas WahlModern computers have the potential to become the most complex artifacts in history. A single microprocessor today, for instance, has the processing power of a billion transistors. The formal methods group works to determine precisely how complex systems behave. It is concerned with formal verification and validation of large-scale computing systems.
Until recently, most of the group’s work has been theoretical. Today, however, the development of highly secure, robust, scalable systems, such as those used in the aerospace industry, is providing a practical platform for its work.
The group is collaborating with NASA on verification technology to assemble space mission systems composed of thousands of component systems. The technology will also have practical applications in fields ranging from computational biology to public health.
The team also conducts formal modeling of obfuscation techniques to defend against malicious attacks. Unlike the network security group, the formal methods group examines the limits of this security approach rather than the performance of specific systems.
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 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.
