The Maude project [1] (and its documentation) may be of interest; they use term rewriting in a formal modeling and model-checking tool. There's an introductory

The Maude project [1] (and its documentation) may be of interest; they use term rewriting in a formal modeling and model-checking tool. There's an introductory course at [2]. 1. http://maude.cs.uiuc.edu/ http://maude.cs.uiuc.edu/ 2. http://heim.ifi.uio.no/~peterol/inf3230-lecturenotes.html http://heim.ifi.uio.no/~peterol/inf3230-lecturenotes.html