Title: Matching mu-logic: A powerful logic for specifying and reasoning about fixpoints and induction, programming languages, and program specification and verification. 

Speaker:  Xiaohong Chen, University of Illinois at Urbana-Champaign, USA

Venue: Seminar Room (Room 334), Building 5, Institute of Software, CAS 

Time: 10:00, May 17th, Friday, 2019 

Abstract: 

　　Matching logic (without mu, shortened as ML) is a first-order logic (FOL) variant for specifying and reasoning about structure by means of patterns and pattern matching. In program verification, ML is used in combination with reachability logic (RL) that takes an operational semantics of a programming language as axioms and yields a program verifier that can prove any reachability properties of any programs written in that language. K framework (http://kframework.org) is a successful implementation of ML and RL. It has been used to define the formal semantics of various real languages such as C, Java, JavaScript, and to verify complex program properties. 

　　However, ML and RL has two main limitations. The first limitation is about the existing proof system of ML, which is only applicable to theories that contain a set of special "definedness symbols" with which equality and membership are defined as derived constructs. The second limitation is that ML and RL can only define and reason about reachability properties and is not capable of expressing liveness or many other interesting properties that temporal or dynamic logics can naturally express. 

　　In this talk, I will address the above two limitations. I will present a new proof system of ML that replaces the existing one without requiring the special "definedness symbols", so it can be applied to all theories. Then, I will present a new logic that extends ML with a mu-binder that builds least fixpoints. The resulting logic is called matching mu-logic (MmL), which is proved to subsume not only ML and RL, but many other important logics/calculi in computer science, especially those which are specifically designed to reason about fixpoints and inductive structures and/or properties, including first-order logic with least fixpoints (LFP), modal mu-logic and many temporal logics such as infinite/finite-trace LTL and CTL, and dynamic logic. At the end of the talk, I will discuss some interesting future work about the new ML proof system and the new MmL logic, including ML/MmL's connection to modal logic, the completeness theorems of ML, and the Henkin semantics of MmL. 

Bio: 

　　Xiaohong Chen (http://fsl.cs.illinois.edu/index.php/Xiaohong_Chen) is a Ph.D. student at University of Illinois at Urbana-Champaign. Before that, he obtained his Bachelor's degree majoring in mathematics at Peking University, China. Xiaohong's main research interest includes formal methods and programming languages, in particular, formal specification and verification and program logics. Xiaohong believes that programming languages and programs should have formal specifications, and verification techniques should be made language-independent.