Bounded Structural Model Finding with Symbolic Data Constraints

TL;DR

This paper introduces the Maude Model Finder (MMF), a native bounded model finding approach within the Maude rewriting logic framework that efficiently generates finite object configurations using symbolic reachability and constraints.

Contribution

The paper presents a novel, native Maude-based bounded model finder that leverages symbolic rewriting, constraint solving, and symmetry reduction without external tools or bespoke generators.

Findings

Proves termination, soundness, and completeness of the bounded construction.

Demonstrates effective symmetry reduction via folding.

Provides a Maude prototype illustrating the approach.

Abstract

Bounded model finding is a key technique for validating software designs, usually obtained by translating high-level specifications into SAT/SMT problems. Although effective, such translations introduce a semantic gap and a dependency on external tools. We present the \emph{Maude Model Finder} (MMF), a native approach that brings bounded model finding to the Maude rewriting logic framework. MMF provides a schema-parametric engine that repurposes symbolic reachability for structural solving, generating finite object configurations from class declarations and graph and data constraints without bespoke generators. Technically, MMF explores a constrained symbolic rewriting system over runtime states modulo an equational theory; SMT is used only to prune states by constraint satisfiability and to discharge entailment checks for subsumption and folding. We contribute a bounded, obligation-driven calculus that separates object creation from reference assignment and supports symmetry reduction by folding via Maude's ACU matching. We establish termination, soundness, and completeness of the bounded construction within the declared bounds, and justify folding via a coverage-preserving subsumption test. We focus on the calculus and its properties, illustrating it on running examples supported by a Maude prototype.