Maude-SE: a Tight Integration of Maude and SMT Solvers
- Maude-SE: a Tight Integration of Maude and SMT Solvers
- YU, GEUNYEOL; BAE, KYUNGMIN
- Date Issued
- 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.
- Article Type
- International Workshop on Rewriting Logic and its Applications (WRLA), page. 220 - 232, 2020-10-22
- Files in This Item:
- There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.