13th Estonian Winter School in Computer Science (EWSCS)
XIII Eesti Arvutiteaduse Talvekool

Palmse, Estonia, March 2-7, 2008

José Meseguer

Dept. of Computer Science
University of Illinois at Urbana-Champaign

Software Specification and Verification in Rewriting Logic


Rewriting logic is a very simple computational logic; it is also highly expressive: it is easy and natural to specify and/or program in it a wide range of systems: distributed object systems, semantics of programming languages, real-time systems, Petri nets, etc. Also, a wide range of logics and inference systems can be specified using rewriting logic as a logical framework.

Once a system has been specified as a rewrite theory, this defines a mathematical model (the initial model of the theory) about which various properties can be specified in various property-oriented logics such as first-order logic, temporal logic, etc. Then, various algorithmic or deductive tools, such as model checkers and theorem provers, can be used to verify those properties.

The course will survey the main ideas of rewriting logic, and its specification and verification aspects. It will also discuss its declarative programming aspects using the Maude language as a vehicle.

Although the course will be self-contained, interested students wanting to prepare for the course might find useful the following two references:

Course materials

Valid CSS! Valid XHTML 1.0 Strict Last changed March 13, 2008 0:00 EET by local organizers, ewscs08(at)cs.ioc.ee
EWSCS'08 page: http://cs.ioc.ee/ewscs/2008/