Rewrite theories are a general and expressive formalism for specifying concurrent systems in which states are axiomatized by equations and transitions among states are axiomatized by rewrite rules. We present a deductive ...

This paper proposes rewriting modulo SMT, a new technique that combines the power of SMT solving, rewriting modulo theories, and model checking. Rewriting modulo SMT is ideally suited to model and analyze reachability ...

Sufficient completeness has been throughly studied for equational specifications, where function symbols are classified into constructors and defined symbols. But what should sufficient completeness mean for a rewrite ...

The InvA tool supports the deductive verification of safety properties of infinite-state concurrent systems. Given a concurrent system specified as a rewrite theory and a safety formula to be verified, InvA reduces such a ...