------------------------------------------------------------------

JAIST/TRUST - AIST/CVS joint workshop on VERIfication TEchnology (VERITE)

Program : 21st Semptember

• Yoshiki Kinoshita (AIST), Brief overview on AIST/CVS
  
  
• Takuya Katayama (JAIST), Perspective of Verifiable and Evolvable e-Society
  
  

• Kokichi Futatsugi (JAIST), Verifying Specifications with Proof Scores
  
  
• Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi (JAIST),
  A Lightweight Integration of Theorem Proving and Model Checking
  
  
• Kenro Yatake, Toshiaki Aoki, Takuya Katayama (JAIST),
  An Object-Oriented Logic for Software Analysis and Design
  
  

• Eun-Hye Choi (AIST), Model checking Web Specifications
  
  
• Sathawornwichit Chaiwat, Takuya Katayama (JAIST),
  A Parametric Model Checking Approach for Real-Time System Design
  
  
• Nguyen Truong Thang, Takuya Katayama (JAIST),
  Specification and Verification of Inter-Component Constraints in CTL
  
  

• Hitoshi Ohsaki (AIST),
  ACTAS - Automated reasoning based on equational tree automata
  
  
• Kunihiko Hiraishi (JAIST),
  Solving Problems on Hybrid Systems by Constraint Satisfaction
  
  

Program : 22nd Semptember

• Peter Dybjer (Chalmers University of Technology)
  Inductive definitions in type theory (Agda demo)
  
  

• Makoto Takeyama (AIST), Towards Agda2
  
  
• Takahiro Seino, Kokichi Futatsugi (JAIST),
  A Toolkit for Generating and Displaying Proof Scores in the OTS/CafeOBJ Method
  
  
• Koichi Takahashi (AIST),
  Abstraction of programs in PML (Pointer Manipulation Language)
  
  

• Toshinori Takai, Daisuke Ikegami (AIST),
  A case study of applying formal methods to developing network system
  
  
• Mizuhito Ogawa (JAIST), Eiichi Horita (NTT), Satoshi Ono (Kogakuin)
  Proving Properties of Incremental Merkle Trees