Research > Formal Methods & Verification
Overview
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.
Faculty
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
Mars Code - Gerard Holzmann 10/7/12
IFAC 2014 - Specification, Verification and Synthesis of Networked Control Systems - Richard Murray 9/18/14
Realtime video from the DARPA Grand Challenge '07 - Richard Murray 9/29/14
Lectures from workshops and events put on by the Keck Institute for Space Studies - Richard Murray 7/30/12
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.