José Meseguer
Dept. of Computer Science
University of Illinois at Urbana-Champaign
USA
Software Specification and Verification in Rewriting Logic
Abstract
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:
- M. Clavel, F. Duran, S. Eker, P. Lincoln, N. Marti-Oliet, J. Meseguer, C. Talcott. All About Maude -- A High-Performance Logical Framework, v. 4350 of Lect. Notes in Comput. Sci.. Springer, 2007.
- J. Meseguer. Software specification and verification in rewriting logic (Lectures at the 2002 Marktoberdorf Summer School). In M. Broy, M. Pizka, eds., Models, Algebras and Logics of Engineering Software, pp. 133-193. IOS Press, 2003.
Course materials
- J. Meseguer. Software specification and verification in rewriting logic. Lecture slides [pdf].
Last changed
March 13, 2008 0:00 EET
by
local organizers, ewscs08(at)cs.ioc.ee
EWSCS'08 page:
//cs.ioc.ee/ewscs/2008/