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.