Research > Formal Methods & Verification

Formal Methods


Formal methods are a crucial tool for the development of large scale, complex systems when reliability and robustness are crucial. By modeling the behavior of systems and mathematically describing the temporal specifications that must be achieved, it is possible to formally verify complex software-controlled systems and certify they behave as desired. When bugs mean the loss of spacecraft, the stakes are high, and so it is easy to see why the work in this area at Caltech is tightly tied to our neighbors at the NASA Jet Propulsion Laboratory. We also collaborate with aerospace companies in developing new approaches to specification, design and verification of safety-critical systems.


Aaron Ames, Joel Burdick, K. Mani Chandy, Gerard Holzmann (Caltech/JPL), Steven Low, Richard Murray, Adam Wierman

Related research groups & Centers > JPL Laboratory for Reliable Software (LaRS), RSRG, CDS

Recent Research Talks

Related Courses

CS 116. Reasoning about Program Correctness.
CS 118. Logic Model Checking for Formal Software Verification.
CS 119. Reliable Software: Testing and Monitoring.
CS/CMS 139. Analysis and Design of Algorithms.
CS/EE 143. Communication Networks.
CS/EE/CMS 144. Networks: Structure & Economics.
CS/EE 145. Projects in Networking.
CS/EE 147. Network Performance Analysis.