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/

2. http://heim.ifi.uio.no/~peterol/inf3230-lecturenotes.html