The Laboratory for Temporal Logic was founded in 2014, and conducts research in rigorous techniques for the formal specification, validation, and verification of safety-critical systems. Our focus includes design-time analysis such as model checking of protocols and system logic, specification debugging, and benchmarking. Our advances in temporal logic analysis during system operation include runtime monitoring and system health management.
Our mission is to advance the state of the art in Formal Methods, specifically model checking, specification debugging, and runtime analysis; develop new technologies that allow for more scalable and efficient analysis techniques, and driving these advances via the goal of creating safer aerospace systems.