|
|
9:50
|
Welcome
and
Introduction
to
the
Workshop
|
Răzvan Diaconescu
Kokichi
Futatsugi
|
|
| 10:00 |
Fostering
Proof Scores in
CafeOBJ
|
Kokichi Futatsugi
|
11:00
|
Guidelines for Formal
Specification and Verification
|
Răzvan Diaconescu
|
12:00
|
Lunch
break
|
14:00
|
An example based
introduction to K
|
Dorel Lucanu |
14:30
|
CIRC prover: an overview
|
Dorel Lucanu |
15:00
|
Proof Events in Computing
|
Petros Stefaneas
|
16:00
|
break
|
16:30
|
Transforming ASN.1
Specifications into CafeOBJ to assist with Property Checking
|
Konstantinos Barlas
|
17:30
|
Algebraic Semantics of
CafeOBJ |
Daniel Găină |
|
10:00
|
Application of Formal
Methods to Binary Code Analysis
|
Akira Mori
|
| 11:00 |
Verifications with Proof
Scores |
Kazuhiro Ogata |
12:00
|
Lunch
break
|
14:00
|
Multiple
Parameters
and
their Instantiation |
Ionuţ Ţuţu |
15:00
|
Implementing CafeOBJ in
Maude |
Chiyo Iida |
16:00
|
break
|
| 16:30 |
Technical
discussions
on
Semantics
and
Proof
Score
Programming
|
|
10:00
|
Formal Analysis of
Risks
in Business Processes
|
Shusaku Iida
|
11:00
|
Formalization and
Verifications of Internal Control
|
Yasuhito Arimoto
|
12:00
|
Lunch break
|
14:00
|
Group
discussions
on
Algebraic
Specifications
and
CafeOBJ
|
|
10:00
|
Constructing
Canonical
Term
Rewriting
Systems
|
Masaki
Nakamura |
11:00
|
How to Prove Equivalence of
Rewriting Systems without (Explicit) Induction
|
Yuki Chiba
|
12:00
|
Lunch
break
|
14:00
|
Technical
Discussion
on
the
Future
Issues
|
15:00
|
Closing
and
coffee
|