Specifying, programming and verifying in Maude

A short-course by Professor Narciso Martí Oliet (Universidad Complutense de Madrid, Spain)


Sep. 22 to Sep. 26, 2014
Instituto de Computação, Universidade Federal Fluminense
(Room to be announced)


The short-course "Specifying, programming and verifying in Maude" will discuss how specifications in Rewriting Logic [1], realized in the Maude system, may be applied in the modeling and validation of algebraic specifications representing different elements of Computer Science such as computational models, communication models, and formal semantics of programming languages.

[1] José Meseguer: Twenty years of rewriting logic. J. Log. Algebr. Program. 81(7-8): 721-781 (2012) DOI: 10.1016/j.jlap.2012.06.003


This short-course is free-of-charge. Registration is required for organizational purposes only. Please write to Christiano Braga (cbraga at ic.uff.br) until August 31, 2014 to register.

Contents and tentative schedule

Morning session: 11:00 to 12:30, afternoon session: 14:30 to 16:00

22/09/2014 - Equational logic

1. Introduction
2. Functional modules
a. Many-sorted equational specifications
b. Order-sorted equational specifications
c. Equational attributes
d. Membership equational logic specifications

23/09/2014 - Rewriting logic and modularization

3. Parameterization
a. Theories and views
b. Data structures
4. System modules
a. Rewriting logic
b. Playing with Maude
c. Lambda calculus

24/09/2014 - Object-oriented specifications

5. Full Maude
6. Object-oriented systems

25/09/2014 - Verification of state transition systems

7. Search and abstraction
8. Model checking
a. LTL and Kripke structures
b. Mutual exclusion
c. Crossing the river

26/09/2014 - Metaprogramming

9. Reflection
a. Maude's metalevel
b. Descent functions
c. Internal strategies
d. Metaprogramming: Rule instrumentation
10. A strategy language for Maude
a. Strategy language syntax
b. Examples
c. Rewriting semantics

Atualizada em 21/7/2014.