Yearly Archives: 2015


CafeOBJ as symbolic and algebraic computation engine

Lecturer Norbert Preining JAIST, Research Center for Software Verification, Japan Place/Time 日本数式処理学会 第24回大会 (24. Annual Meeting of the Japan Society for Symbolic and Algebraic Computation) 2015-06-16, Tsukuba University, Tsukuba, Japan. Abstract CafeOBJ is an algebraic specification language based on equational order-sorted logic, which incorporates rewriting logic and hidden algebras. What […]


Tutorial: Lists 1

This second in a series of tutorials will introduce you to functional programming the CafeOBJ way, in particular will we discuss lists and various ways to implement, use, and abuse the. We expect a running CafeOBJ interpreter being available. For a first steps tutorial, please consult .


Introduction to CafeOBJ with case study

Lecturer Norbert Preining JAIST, Research Center for Software Verification, Japan Place/Time IMI, Kyushu University, 2015-03-13, Hakata, Japan. Abstract Systematic construction and verification of specifications is still one of the most important challenges in system development aka engineering. We present our approach to this problem, an executable algebraic specification language, CafeOBJ. […]


Verification of Real-World Security Protocols in CafeOBJ: A Case Study of PACE

Lecturer Dominik Klein Federal Office for Information Security, Germany Place/Time JAIST Tokyo Satellite Campus Shinagawa, Room B 2015/02/26 (Thu) 15:00 to 17:00 Abstract The ICAO-standardized Password Authenticated Connection Establishment (PACE) protocol is used all over the world to secure access to electronic passports. Key-secrecy of PACE is proven by first […]


CafeOBJ 1.5.3 released 1

We have released a new version of CafeOBJ, which incorporates besides other fixes the following changes: interpreter functions ‘describe module tree’ (new) – prints out module importing structure ‘show modules’ – does not print out hidden modules new abbreviations: tr, ctr, pd, pds, bpd, bpds (for trans, ctrans, pred, preds, […]