Zoom: https://illinois.zoom.us/j/5494764956?pwd=MDNnaE5CWG0yRVlEZWl5bldoRnErZz09
Abstract:
Computer programs are getting more complicated and safety-critical these days. Formal methods tools such as program verifiers build mathematical models for programs and formally prove that programs have the desired properties. However, these tools are complicated and work like a "black box," so we have to trust them for what they claim about our programs, resulting in a large "trust base" in today's program reasoning. My research aims at reducing this trust base and improving the reliability and trustworthiness of formal methods tools.
In this talk, I will present a unifying foundation for specifying and reasoning about programs, based on matching logic (http://matching-logic.org). Matching logic is a simple logic with high expressive power. Various programming languages and paradigms can be uniformly specified using axioms/notations. Various program properties can be specified using formulas and reasoned about using one fixed set of formal proof rules. As a result, the correctness of programs and program reasoning tools can be certified using rigorous and machine-checkable proof certificates, which can be automatically checked using a small proof checker, thus reducing the trust base of program reasoning.
Bio:
Xiaohong Chen is a Ph.D. candidate in the computer science department at UIUC, advised by Prof. Grigore Rosu. Xiaohong's research interests are in logic, formal methods, and programming languages, with a focus on using rigorous machine-checkable proof certificates to reduce the trust base of various programming language tools. Xiaohong's research on matching logic (http://matching-logic.org) as a unifying foundation for programming has helped improve the safety and reliability of the K language framework (https://kframework.org). Xiaohong is the recipient of the Yunni and Maxine Pao Memorial Fellowship, the Mavis Future Faculty Fellowship, and the Graduate School Dissertation Completion Fellowship. His research proposal has been funded by the Ethereum Foundation for its potential to make smart contracts more trustworthy and transparent. More information at https://xchen.page/.
https://wiki.illinois.edu/wiki/display/grad/PILOT+SEMINAR
