Panagiotis Manolios

Thomas Wahl

Modern 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.