Title: Rapid Development of Mechanized Semantics
Advisors: Zach Tatlock and Michael Ernst
Supervisory Committee: Zach Tatlock (co-Chair), Michael Ernst (co-Chair), Jason Detwiler (GSR, Physics), and Sergey Levine
Abstract: Formal verification using modern proof assistants provides high assurance that a program behaves according to its specification. However, applying these techniques to a program requires suitable formal semantics for the programming language in use, and designing semantics for new languages is a lengthy process. We propose a new approach to the design of language semantics, using a simple intermediate language and differential testing to rapidly develop semantics that reflect the behavior of existing language implementations. We plan to evaluate this approach by applying it to the Clinical Neutron Therapy System, a complex medical installation, by designing semantics, verifying program properties, and developing verified language implementations for safety-critical components written in a variety of languages.