センター長挨拶Policy Statement研究テーマ研究活動研究成果Technical Reports書籍共同研究集会支援English
 研修コース ・ニュースレター ・CVS Staff ・アクセス 採用情報  ・お問い合わせ ・更新履歴 ・プレスリリース ・カレンダーHOME 

3rd AIST/CVS Workshop 18th April 2005
Last updated: 2005.04.18


Workshop on Automatic and Interactive Verification

日    程: 2005年4月18日(月)
場    所: システム検証研究センター千里オフィス6F会議室       地図はこちら
概    要: 
アルゴリズミックな自動検証と人知を活かせる対話型の検証の効果的な組み合わせについて討議する、一日ワークショップのご案内です。両者の融合の 研究はそれぞれのコミュニティーで盛んですが、お互いが他方の研究を深く理解するには、意識的に一つのコミュニティーを形成していく機会がまだまだ多く必 要となります。Illinois大José Meseguer教授、Chalmers大Thierry Coquand, Peter Dybjer, Bengt Nordström三教授他、当研究センターがそれぞれの分野で協力関係にある研究者の同時来日を機会に、そのような一つのコミュニティーの形成の資する のが本一日ワークショップの目的です。皆様のご参加をお待ちしています。

This is a call for participation for the 1-day "Workshop on Automatic and Interactive Verification", aimed to promote discussions on effective combinations of automatic, algorithmic verification and interactive one guided by users' insight. The topic has been actively studied in both of the two research communities, but efforts are still needed to deepen understanding of each other. The workshop is one such effort to develop a single community, with talks given by researchers collaborating with CVS in those related fields [Prof. José Meseguer(Illinois), Profs. Thierry Coquand, Peter Dybjer, Bengt Nordström(Chalmers)].

Meeting Room, 6th floor of Mitsui Sumitomo kaijo Senri Bldg.., at CVS Senri site, AIST Kansai     MAP


09:00 --09:45 José Meseguer (University of Illinois)
Logical and Meta-Logical Frameworks: The Rewriting Logic Experience
15 min break
10:00 -- 10:25 Peter Dybjer (Chalmers University of Technology)
Combining Verification Methods in Software Development: an Overview of Research Project at Chalmers
10:25 -- 11:10 Thierry Coquand (Chalmers University of Technology)
Connecting Agda with external tools for FOL and rewrite systems
20 min break for informal discussion
11:30 -- 12:00 Whole group discussion:
(on rewriting and type-theory based interactive proof assistant)
12:00 -- 12:30 Hitoshi Ohsaki (CVS)
Tree Automata and System Verification
12:30 -- 14:00 Lunch
14:00 -- 14:30 Yoshinori Tanabe (CVS)
An Approach to Verification of Pointer Manipulating Systems Using Temporal Logic Formulas
14:30 -- 15:00 Yoshiki Kinoshita (CVS)
A Scenario of Integrated Verification Environment Based on Agda
30 min break for informal discussions
15:30 -- 16:00 Bengt Nordström (Chalmers University of Technology)
Proof Documents: Presentation and Representation
16:00 -- 17:30 Whole group discussion: on integration of automatic and interactive verification
18:00 -- Workshop Banquette (at the venue)


Logical and Meta-Logical Frameworks: The Rewriting Logic Experience
José Meseguer
University of Illinois
A logic framework is a logic with good properties to represent other logics in it, so that we can mimic deduction in the original logic as deduction in the framework logic. A meta-logical framework is a logical framework in which, in addition, we can do meta-logical reasoning about the logics that we represent in it. The talk will discuss logical and meta-logical frameworks in terms of an axiomatic theory of general logics, and will report on the experience using rewriting logic as a logical and meta-logical framework, exploiting features such as reflection and initiality.

産総研ホーム > 組織 > 研究センター > システム検証研究センター
Copyrights (C) 2005-2009 AIST Research Center for Verification and Semantics, All Rights Reserved.