Initial algebra semantics provides a generic and principled framework to study induction. In this paper, we give a complete formalization of ini- tial algebra semantics and inductive reasoning using matching logic—a small and unifying logic for formal semantics of programming languages. Specifi- cally, we define initial algebra semantics as matching logic theories and derive induction/iteration/primitive-recursion principles as formal theorems within matching logic, using its proof system. This way, we obtain, for the first time, a rigorous logical foundation for general initial algebra semantics and induc- tion, both proof-theoretically and model-theoretically. As a bonus, matching logic admits the smallest known proof checker for a logic supporting inductive proofs, of only 240 lines of code.

Abstract We present a sound and complete axiomatization of finite words using matching logic. A unique feature of our axiomatization is that it gives a shallow embedding of regular expressions into matching logic, and a logical representation of finite automata. The semantics of both expressions and automata are precisely captured as matching logic formulae that evaluate to the corresponding language. Regular expressions are matching logic formulae as is, while the embedding of automata is a structural analog—computational aspects of automata are captured as syntactic features. We demonstrate that our axiomatization is sound and complete by showing that runs of Brzozowski’s procedure for equivalence checking correspond to matching logic proofs. We propose this as a general methodology for producing machine-checkable formal proofs, enabled by capturing structural analogs of computational artifacts in logic. The proofs produced can be efficiently checked by the Metamath Zero verifier. Work presented in this paper contributes to the general scheme of achieving verifiable computing via logical methods, where computations are reduced to logical reasoning, encoded as machine-checkable proof objects, and checked by a trusted proof checker.

Previous work on rewriting and reachability logic establishes a vision for a language-agnostic program verifier, which takes three inputs: a program, its formal specification, and the formal semantics of the programming language in which the program is written. The verifier then uses a language-agnostic verification algorithm to prove the program correct with respect to the specification and the formal language semantics. Such a complex verifier can easily have bugs. This paper proposes a method to certify the correctness of each successful verification run by generating a proof certificate. The proof certificate can be checked by a small proof checker. The preliminary experiments apply the method to generate proof certificates for program verification in an imperative language, a functional language, and an assembly language, showing that the proposed method is language-agnostic.

Abstract We pursue the vision of anideal language framework, where programming language designers only need to define the formalsyntaxandsemanticsof their languages, and all language tools are automatically generated by the framework. Due to the complexity of such a language framework, it is a big challenge to ensure its trustworthiness and to establish the correctness of the autogenerated language tools. In this paper, we propose an innovative approach based onproof generation. The key idea is to generate proof objects as correctness certificates for each individual task that the language tools conduct, on a case-by-case basis, and use a trustworthy proof checker to check the proof objects. This way, we avoid formally verifying the entire framework, which is practically impossible, and thus can make the language framework bothpracticalandtrustworthy. As a first step, we formalize program execution as mathematical proofs and generate their complete proof objects. The experimental result shows that the performance of our proof object generation and proof checking is very promising.

The K framework (kframework.org) is an effort in realizing the ideal language framework, where programming languages must have formal semantics and all language tools are automatically generated from the formal semantics. Until recently, K has been developed as an engineering endeavor driven by challenges such as formalizing the complete semantics of large languages (C, Java, JavaScript, Python, etc), but deriving its semantics from translations to various formalisms, such as rewriting logic, graph transformations, or Coq. This semantics borrowing approach came not only at a notational cost, where the original language meaning was ``lost in translation'', but also at a foundational cost: the target formalisms were more complicated than necessary, yet more restricted due to their prescribed ways to define language semantics.

Automation of fixpoint reasoning has been extensively studied for various mathematical structures, logical formalisms, and computational domains, resulting in specialized fixpoint provers for heaps, for streams, for term algebras, for temporal properties, for program correctness, and for many other formal systems and inductive and coinductive properties. However, in spite of great theoretical and practical interest, there is no unified framework for automated fixpoint reasoning. Although several attempts have been made, there is no evidence that such a unified framework is possible, or practical. In this paper, we propose a candidate based on matching logic, a formalism recently shown to theoretically unify the above mentioned formal systems. Unfortunately, the (Knaster-Tarski) proof rule of matching logic, which enables inductive reasoning, is not syntax-driven. Worse, it can be applied at any step during a proof, making automation seem hopeless. Inspired by recent advances in automation of inductive proofs in separation logic, we propose an alternative proof system for matching logic, which is amenable for automation. We then discuss our implementation of it, which although not superior to specialized state-of-the-art automated provers for specific domains, we believe brings some evidence and hope that a unified framework for automated reasoning is not out of reach.

We propose a novel definition of binders using matching logic, where the binding behavior of object-level binders is directly inherited from the built-in exists binder of matching logic. We show that the behavior of binders in various logical systems such as lambda-calculus, System F, pi-calculus, pure type systems, can be axiomatically defined in matching logic as notations and logical theories. We show the correctness of our definitions by proving conservative extension theorems, which state that a sequent/judgment is provable in the original system if and only if it is provable in matching logic, in the corresponding theory. Our matching logic definition of binders also yields models to all binders, which are deductively complete with respect to formal reasoning in the original systems. For lambda-calculus, we further show that the yielded models are representationally complete, a desired property that is not enjoyed by many existing lambda-calculus semantics. This work is part of a larger effort to develop a logical foundation for the programming language semantics framework K (http://kframework.org).

K framework is an effort in realizing the ideal language framework where programming languages must have formal semantics and all languages tools are automatically generated from the formal semantics in a correct-by-construction manner at no additional costs. In this extended abstract, we present matching mu-logic as the foundation of K and discuss some of its applications in defining constructors, transition systems, modal mu-logic and temporal logic variants, and reachability logic.

Matching logic is a logic for specifying and reasoning about structure by means of patterns and pattern matching. This paper makes two contributions. First, it proposes a sound and complete proof system for matching logic in its full generality. Previously, sound and complete deduction for matching logic was known only for particular theories providing equality and membership. Second, it proposes matching μ -Iogic, an extension of matching logic with a least fixpoint μ -binder, It is shown that matching μ -Iogic captures as special instances many important logics in mathematics and computer science, including first-order logic with least fixpoints, modal μ -Iogic as well as dynamic logic and various temporal logics such as infinite/finite-trace linear temporal logic and computation tree logic, and notably reachability logic, the underlying logic of the \mathbbk framework for programming language semantics and formal analysis. Matching μ -logic therefore serves as a unifying foundation for specifying and reasoning about fixpoints and induction, programming languages and program specification and verification.

Coordination is playing a key role in complex cyber-physicalsystems (CPSs). The complexity and importance of coordination models and languages for CPSs necessarily lead to a higher relevance of testing during development of CPSs. Model-based testing is a promising technology to test the conformance or non-conformance relation between the implementation-under-test (IUT) and its specification. In this paper, we present an approach to test the conformance relation tiococ(Timed Input-Output Conformance) between the implementation of a timed Reo connector and its specification given by a timed constraint automaton (TCA). An algorithm to generate test cases from a TCA is proposed and the testing approach is implemented in UPPAAL.