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 […]
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 […]
Lecturer Norbert Preining JAIST, Research Center for Software Verification, Japan Place/Time WADT 2014: 22nd International Workshop on Algebraic Development Techniques September 2014, Sinaia, Romania. Abstract One methodolgy for formal specification of a complex system is by using Abstract State Machine (Asm). Here states describe the actual state of the system, […]
A case study for meta-level specifications Lecturer Norbert Preining JAIST, Research Center for Software Verification, Japan Place/Time JAIST Collaboration Room 6 (I57-g) 2014/08/07 (Thu) 15:00 to 17:00 Abstract We provide an innovative development of algebraic specifications and proof scores in CafeOBJ by extending a base specification to the meta-level that […]
Lecturer Norbert Preining JAIST, Research Center for Software Verification, Japan Place/Time 14th International Workshop on Termination July 2014, Vienna, Austria. Abstract We provide an innovative development of algebraic specifications and proof scores in CafeOBJ of QLock’s safety and liveness properties. The particular interest of the development is two-fold: Firstly, it […]
Lecturer Kokichi Futatsugi JAIST, Research Center for Software Verification, Japan Place/Time JAIST Collaboration Room 6 (I57-g) 2014/07/03 (Thu) 15:00 to 17:00 Abstract A new method for verification of transition systems is presented. The state space of a transition system is defined as a quotient set (i.e. a set of equivalence […]