Our center focuses on the formal specification and verification of hardware and software systems. We invent new mathematically-based techniques, languages, and tools to model the behavior of systems and to verify that these models satisfy desired properties. We also use our tools to find bugs in hardware and software designs. Thus, our approach of using formal methods complements the more traditional approaches of simulation and testing.

Our challenges are in modeling large, complex systems and in verifying behavioral properties of concurrent, distributed, real-time, and resource-constrained systems. To meet these challenges, we do fundamental research on data structures and algorithms, data and control abstractions, specification logics, and compositional proof techniques; we build tools such as model checkers, proof checkers, and combinations of the two; we apply our methods to a diverse range of applications: automotive controllers, circuit designs, communication protocols, disk arrays, distributed simulation architectures, file systems, networked systems, robots, security protocols, and spacecraft.

Thanks to our sponsors: ARO, NASA, and NSF.