Maude-SE: a Tight Integration of Maude and SMT Solvers

Abstract

This paper presents Maude-SE, an SMT extension of Maude that tightly integrates Maude and SMT solvers with extra functionality. In addition to the existing SMT solving capability of Maude, the tool provides three additional features that are not currently supported by Maude but that are very useful for rewriting modulo SMT: (i) building satisfying assignments by SMT solving, (ii) simplifying formulas using the underlying SMT solver, and (iii) dealing with non-linear arithmetic formulas. Hence, Maude-SE can analyze nontrivial systems that cannot be dealt with by the previous Maude-SMT implementation.