Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
10329406 | Electronic Notes in Theoretical Computer Science | 2005 | 18 Pages |
Abstract
Rewriting logic is a very expressive formalism for the specification of concurrent and distributed systems; more generally, it is a logic of change. In contrast, VLRL is a modal logic built on top of rewriting logic to reason precisely about that change. Here we present a technique to mechanically prove VLRL properties of rewrite theories using the reflective capability of rewriting logic through its Maude implementation.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Isabel Pita, Miguel Palomino,