Activities


CafeOBJ Tutorial at ICFEM 2016

Lecturer FUTATSUGI, Kokichi OGATA, Kazuhiro JAIST, Japan Place/Time 2016-11-15 10:00-17:30, TKP Ichigaya Conference Center, Tokyo, Japan. Web site Please see this page for details. Abstract CafeOBJ is a most advanced algebraic formal specification language system with rewriting/reduction engine which can be used for interactive verification. Proof scores are scripts for […]


ESSLLI 2016 Course: Algebraic Specification and Verification with CafeOBJ

During this year’s ESSLLI (European Summer School in Logic, Language and Information) I was teaching a course on Algebraic Specification and Verification with CafeOBJ. Please this post for the course materials like slides and code example. Abstract Ensuring correctness of complex systems like computer programs or communication protocols is gaining […]


CafeOBJ 1.5.5 released

We have released a new version of CafeOBJ, which incorporates besides other fixes the following changes: Enhancemets of a family of Bool term inspector commands: binspect [ in : <Modexpr> ] <bool-term> . converts given <bool-term> into abstracted xor-and normal form bshow [ tree | grind ] shows abstracted Bool […]


Specification and Verification with Proof Scores in CafeOBJ

Lecturer FUTATSUGI, Kokichi JAIST, Research Center for Software Verification, Japan Place/Time 2015-10-23 and 10-30, NII, Tokyo, Japan. Web site Please see this page for details. Abstract CafeOBJ is a most advanced algebraic formal specification language system with rewriting/reduction engine which can be used for interactive verification. Proof scores are scripts […]


CafeOBJ course at the ESSLLI 2016 2

The European Summer School in Logic, Language and Information ESSLLI is a yearly event that normally brings together several hundred students and teachers for two weeks of courses. Next year’s ESSLLI 2016 will be held in Bozen, Italy. One of the courses will be Algebraic Specification and Verification – an […]


CafeOBJ 1.5.4 released

We have released a new version of CafeOBJ, which incorporates besides other fixes the following changes: CITP changes new commands :ctf- and :csp- new command :def(ine) to turn :ctf(-) and :csp(-) into proper tactics for :apply new tactics nf, ct improvements in the online help system bug fixes in AC […]


Algebraic specifications and Functional programming with CafeOBJ

Lecturer Norbert Preining JAIST, Research Center for Software Verification, Japan Place/Time Mathematical Software and Free Documents XXI 2015-09-12, Kyoto, Japan. Abstract CafeOBJ is an algebraic specification language based on equational order-sorted logic, which incorporates rewriting logic and hidden algebras. What sets it apart from other specification languages is that it […]


Getting CafeOBJ via MacPorts

I have finally finished the Portfile for CafeOBJ, which allows users to install CafeOBJ via the usual port command of MacPorts. For one needs to add our local source (which only ships CafeOBJ port), but I hope to get the port into the standard distribution soon. Necessary steps: Add the […]


Zick-zacking through the CafeOBJ’s vegetable garden

Lecturer Norbert Preining JAIST, Research Center for Software Verification, Japan Place/Time 43rd TRS Meeting 2015-09-09, Morioka, Japan. Abstract We are exploring a variety of topic related to CafeOBJ: History and background, symbolic calculations and polynoms, computation and exact reals, liveness properties for state machine based specifications, and news from CITP/CafeOBJ, […]


A Maude environment for CafeOBJ

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 […]