Research > Formal Methods & Verification

Formal Methods

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.


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.
Department of Computing + Mathematical Sciences