Norbert Preining


CafeOBJ 1.6.0 released

We have released a new version of CafeOBJ, which incorporates the following changes: CITP is officially renamed to PTcalc documents are not updated yet PTcalc (CITP) enhancements :init defined by :def is evaluated in the proof node to which it is applied :init can be without substitution Search predicate enhancements […]


CafeOBJ 1.5.9 released

We have released a new version of CafeOBJ, which incorporates the following changes: improved memoization higher heap allocation on 64bit systems fixes to .cafeobj file handling new switch ‘show every finding’ optimization fixes and dead code removal Please see the download page for the source release, binary packages, and installation […]


CafeOBJ 1.5.8 released

We have released a new version of CafeOBJ, which incorporates new commands and fixes for CITP. Please see the download page for the source release, binary packages, and installation instructions. For the moment Windows builds are only available based on Allegro CL due to incompatibilities between Windows SBCL and CafeOBJ. […]


CafeOBJ 1.5.7 released

We have released a new version of CafeOBJ, which incorporates mostly fixes for CITP as well as updates to work with newer versions of SBCL. Please see the download page for the source release, binary packages, and installation instructions. For the moment Windows builds are only available based on Allegro […]


Book published: Introduction to programming for model description and validation (in Japanese)

Prof. Futatsugi’s book Introduction to programming for model description and validation (モデルの記述と検証のためのプログラミング入門) has been published this week and will be available from various outlets and online. The web site of the book provides access to downloadable versions of the code given in the book.


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