The Maude LTL Model Checker

Steven Eker, José Meseguer and Ambarish Sridharanarayanan

The Maude LTL model checker supports on-the-fly explicit-state model checking of concurrent systems expressed as rewrite theories with performance comparable to that of current tools of that kind, such as SPIN. This greatly expands the range of applications amenable to model checking analysis. Besides traditional areas well supported by current tools, such as hardware and communication protocols, many new applications in areas such as rewriting logic models of cell biology, or next-generation reflective distributed systems can be easily specified and model checked with our tool.

(BibTeX entry)    (gzip'ed Postscript)   


back   home   Formal Methods and Declarative Languages Laboratory   Computer Science Laboratory, SRI International