Papers for

program verification developers

Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.

Model composition methods that preserve logic proofs in software design

Dependently Typed Model Composition for Matching Logic

Abstract: This paper investigates model composition—often referred to as "gluing"—within the framework of matching logic. Specifically, we examine the systematic combination of existing signatures, variable valuations, theories, and their corresponding models. Our primary objective is to ensure that this composition preserves satisfaction proofs; that is, any theory validated by the individual constituent models is also validated by the resulting composite model. Our definitions are based on a polyadic, sorted variant of matching logic, which has also been expressed in the Rocq proof assistant. Therefore, we outline our definitions with dependent types for this work to serve as a direct blueprint for the mechanization in the short-term future.

Mon 28 SeptLogic in Computer Science
The gist
Sometimes when combining parts of a software system, it is tricky to ensure that the combined system still follows all the rules each part followed separately. The authors look at a way to combine these parts—called models—using a logical framework called matching logic. They make sure that if each part satisfies certain rules, then the combined model does too. Their work uses detailed type systems to make it easier to check these combinations automatically in computer proof tools.
Open → 2609.34892v1