Lecturer Norbert Preining JAIST, Research Center for Software Verification, Japan Place/Time 日本数式処理学会 第２４回大会 (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 […]
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 this post.
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. […]
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 […]
Lecturer Kokichi Futatsugi JAIST, Research Center for Software Verification, Japan Place/Time JAIST IS school seminar room 9F 2015/02/26 (Thu) 15:00 to 17:00 Abstract Generic proof scores for the generate & check method in CafeOBJ are presented. The generic proof scores codify the generate & check method as parameterized modules in […]
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, […]
This tutorial will guide you through starting the CafeOBJ interpreter, and some simple calculations. We will also give a very short introduction to the logic background of CafeOBJ, and the basic structure of the language.