A Flexible Framework for Integrating Maude and SMT Solvers Using Python

This paper presents a new implementation of Maude-SE that provides a flexible yet efficient framework for connecting Maude to SMT solvers. There exist previous implementations to integrate Maude and SMT solvers at the C++ level, but they do not support uninterpreted functions and folding reduction, and are very difficult to customize. The new version of Maude-SE supports uninterpreted functions, symbolic reachability analysis with folding, and an abstract Python connector that makes it easy to integrate and customize SMT solving with Maude using its Python API, without having to understand Maude’s internal implementation and recompile the source code.