Lecturer
Adrián Riesco Rodríguez
Universidad Complutense de Madrid DSIC (Departamento de Sistemas Informáticos y Computación), Madrid, Spain
Place/Time
JAIST IS school seminar room 9F
2015/08/27 (Thu) 14:00 to 17:00
Abstract
CafeOBJ and Maude are sister languages of the OBJ language, and two of the most advanced formal specification languages for systems verification. Although both of them have a similar syntax and semantics, different usages and applications have been developed for them. Hence, a tool combining both languages would be very useful for exploiting the specific features of each of them.
In this talk we present the latest developments on the Maude environment for CafeOBJ. This environment allows CafeOBJ specifications to be loaded into the Full Maude database, hence providing a simple way to use Maude tools in CafeOBJ specification. This is specially interesting when using Proof Scores including search predicates, since Maude can traverse the search space in a very efficient way and provide results that in some cases are beyond CafeOBJ performance.