Z^[AbPolicy Statementbe[}bbbTechnical ReportsbbbWxbEnglish CR[X Ej[X^[ ECVS Staff EANZX E̗p  E₢킹 EXV EvX[X EJ_[ EHOME

# CVS/AIST WORKSHOP SERIES

## ONE-DAY WORKSHOP ON VERIFICATION AND REWRITING 2004/10/21

On the occasion of Prof. J. Meseguer's visit to CVS/AIST and Prof. Buchberger's visit to Kyoto, we organise a one day workshop on verification and rewriting. Anyone interested in the talks are welcome. Those who wish to attend are kindly asked to send an application form, attached to the end of this message, to workshop-on-verification-and-rewriting@m.aist.go.jp to help preparation.

PLACE:
Meeting Room, 2nd floor of the E building Amagasaki site, AIST Kansai

### TENTATIVE PROGRAM:

There may be more/less speakers and speakers may have other thoughts about the title and contents of their talks; this program is subject to change at any moment until the day of workshop!

10:00-10:50      Jose Meseguer
Title and Abstract To Be Announced

11:00-11:50      Hitoshi Ohsaki
Reachability Analysis Based on AC-tree Automata Technique

11:50-13:20      Lunch

13:20-14:10      Bruno Buchberger
The Theorema Project: An Overview

14:20-14:50      Makoto Takeyama
An Integrated Verification Environment

14:50-15:20      Break

15:20-16:10      Masahiko Sato
A Simple Theory of Expressions, Judgments and Derivations

16:20-17:10      Yoshinori Tanabe
Satisfiability checking of temporal logics for
verification of pointer systems

18:00-             Dinner

### ABSTRACTS OF TALKS:

Hitoshi Ohsaki
Research Center for Verification and Semantics (CVS),
National Institute of Advaced Industrial Science and Technology (AIST)

TITLE:
Reachability Analysis Based on AC-tree Automata Technique

ABSTRACT:
In this talk a verification tool called ACTAS, e.g for security protocols, based on AC-tree automata theory is introduced. ACTAS is an integrated system for manipulating associative and commutative tree automata (AC-tree automata for short), that has various functions such as for Boolean operations of AC-tree automata, computing rewrite descendants, and solving emptiness and membership problems. In order to deal with high-complexity problems in reasonable time, over-and under-approximation algorithms are also equipped.

Such functionality enables us automated verification of safety property in infinite state models, that is helpful in the domain of, e.g. network security, in particular, for security problems of cryptographic protocols allowing an equational property. In runtime of model construction, a tool support for analysis of state space expansion is provided. The intermediate status of the computation is displayed in numerical data table, and also the line graphs are generated.
Besides, a graphical user interface of the system provides us a user-friendly environment for handy use.

Bruno Buchberger
Professor of Computer Mathematics Research Institute for Symbolic Computation Johannes Kepler University, A4232 Castle of Hagenberg, Austria

TITLE:
The Theorema Project: An Overview

ABSTRACT:
The Theorema project aims at supporting, by algorithms, the process of mathematical theory exploration. We study all phases of this process from concept invention to proposition invention and proof, problem invention, and algorithm invention and verification. The final goal is the flexible build-up of well structured, formal, verified mathematical knowledge bases including algorithm libraries and a tool box for working with such knowledge bases. The project is based on previous research experience in the area of computer algebra, notably the theory of Groebner bases.

In the talk I will describe the basic ideas and the current state of the project. A particular emphasis will be laid on recent results on algorithm-supported algorithm synthesis. I will also give some examples of the currently available tools in the Theorema system.

Makoto Takeyama
Research Center for Verification and Semantics (CVS),
National Institute of Advaced Industrial Science and Technology (AIST)

TITLE:
An Integrated Verification Environment

ABSTRACT:
We outline our plan for an integrated developing envrionment for systems verification. Its aim is to integrate variety of verification methods and tools into a coherent whole: high-level model description, abstraction, model-checking, and interactive theorem proving. We explain aspects of the methodology supported by such an environment.

Masahiko Sato
Graduate School of Informatics, Kyoto University

TITLE:
A Simple Theory of Expressions, Judgments and Derivations

ABSTRACT:
We propose a simple theory of expressions which is intended to be used as a foundational syntactic structure for the Natural Framework (NF). We define expression formally and give a simple proof of the decidability of $\alpha$-equivalence. We use this new theory of expressions to define judgments and derivations formally, and we give concrete examples of derivation games to show a flavor of NF.

Yoshinori Tanabe

TITLE:
Satisfiability checking of temporal logics for verification of pointer systems

ABSTRACT:
Hagiya and Takahashi has proposed a method of abstraction for graph rewriting systems, which uses temporal logics and is suitable for describing properties of pointer systems. We have started designing a verification tool based on the method. Satisfiability checking plays an important role for verification using abstraction and therefore should be a key part in our tool. In this talk algorithms for deciding satisfiability in variants of CTL, their implementation with BDD, and relationship to pointer systems are presented.

CVS/AIST ONE DAY WORKSHOP ON VERIFICATION AND REWRITING 2004/10/21

APPLICATION FORM
Send this form to workshop-on-verification-and-rewriting@m.aist.go.jp before 20 October.

NAME:

AFIILIATION: