Talk


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


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


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


CafeOBJ for real

Using an algebraic specification language as theorem prover for computational reals Lecturer Norbert Preining JAIST, Research Center for Software Verification, Japan Place/Time CCA 2015 Twelfth International Conference on Computability and Complexity in Analysis 2015-07-15, Tokyo, Japan. Abstract CafeOBJ is a many- and order-sorted algebraic specification language from the OBJ family, […]


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


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


Liveness properties in CafeOBJ

A case study for meta-level specifications Lecturer Norbert Preining JAIST, Research Center for Software Verification, Japan Place/Time LOPSTR 2014: Logic-Based Program Synthesis and Transformation September 2014, Canterbury, UK. Abstract We provide an innovative development of algebraic specifications and proof scores in CafeOBJ by extending a base specification to the meta-level […]