How can we reason about safety-critical systems, such as aircraft and spacecraft, to determine whether they
behave safely? How can we formalize system requirements and enable automated specification debugging? How can we reason about large spaces of possible designs from the early system design phase? How can we carry through formal verification to runtime, enabling autonomous operation via intelligent, on-board system health management?
Read more
