K | Runtime Verification Inc
Matching logic is a unifying foundational logic for programming languages, specification, verification. It serves as the foundation of the K framework : a formal language framework where all programming languages must have a formal semantics and all language tools are automatically generated by the framework from the semantics at no additional costs, in a correct-by-construction manner.
Traditionally, concrete behaviors of programs are defined by operational semantics , while the properties of them are specified and proved using axiomatic semantics , such as Hoare logic . Unfortunately, axiomatic semantics of real languages are rather complex, so correctness proofs are necessary in order to trust the proven properties. Moreover, such proofs have to be maintained as the language changes, which is generally perceived as a burden. Ideally, we would like to have only one reference language sem
Matching logic allows us to regard a programming language through both operational and axiomatic lenses at the same time, making no distinction between the two. The semantics of a programming language is given in matching logic as a set of rewrite rules. Both operational behaviors and formal properties of a program are derived using the language-independent proof system of matching logic. That is, we use the same proof system to reason about all programming languages, which is different from the classic axi
K | Runtime Verification Inc