|
14:00
|
Opening
|
Răzvan Diaconescu
|
14:15
|
Introduction to the School
|
15:30
|
Break
|
16:00-17:15
|
Verifying Specifications
with Proof Scores in CafeOBJ
-- An overview of formal verifications in CafeOBJ --
|
Kokichi Futatsugi
|
|
9:30
|
Basics of Modeling,
Specification, and Verification
|
Kokichi Futatsugi |
11:00
|
Break
|
11:30
|
Models and Structuring of
Specifications
|
Kokichi Futatsugi |
13:00
|
Lunch
break
|
15:00
|
Exercises
|
16:30-17:30
|
Discussions
|
|
9:30
|
Reasoning by Rewriting
|
Masaki Nakamura
|
11:00
|
Break
|
11:30
|
Verification by Induction
|
Masaki Nakamura
|
13:00
|
Lunch
break
|
15:00
|
Exercises
|
16:30-17:30
|
Discussions
|
|
9:30
|
Modeling and Specification
in OTS/CafeOBJ (QLOCK example)
|
Kokichi Futatsugi |
11:00
|
Break
|
11:30
|
Verification with Proof
Score (QLOCK example)
|
Kokichi Futatsugi |
13:00
|
Lunch
break
|
15:00
|
Exercises
|
16:30-17:30
|
Discussions
|
|
9:30
|
Analysis of Alternating
Bit Protocol (1) -- Modeling and Specification
|
Kazuhiro Ogata
|
11:00
|
Break
|
11:30
|
Analysis of Alternating
Bit Protocol (2) -- Verification
|
Kazuhiro Ogata
|
13:00
|
Lunch
break
|
15:00
|
Exercises
|
16:30-17:30
|
Discussions
|
|
Student Workshop
|
9:30
|
Patterns for Maude
Metalanguage Applications
|
Eugen-Ioan
Goriac
|
9:50
|
Modeling and
Verification of Mobile Systems using CafeOBJ
Algebraic Specification Language
|
Iakovos
Ouranos
|
10:10
|
Applying algebraic specification techniques to model real time
authentication protocols: The TESLA protocol case verified with
CafeOBJ
|
Kostantinos
Barlas
|
10:30
|
|
Spyros
Komninos
|
11:00
|
Break
|
11:30
|
Tense operators on
Lukasiewicz-Moisil algebras
|
Denisa
Diaconescu
|
11:50
|
Free theorems for refinement of behavioral specifications
|
Marius
Petria
|
12:10
|
Integrating
VSE's refinement in HETS
|
Mihai
Codescu
|
12:30
|
Order sorted algebra
|
Daniel
Găină
|
|
|
Free
discussions
|
|
9:30
|
Case studies with Proof
Scores
|
Kazuhiro Ogata
|
11:00
|
Break
|
11:30
|
Falsification and
Verification by Searching
|
Kokichi Futatsugi
|
13:00
|
Lunch
break
|
15:00
|
Exercises
|
16:30-17:30
|
Discussions
|