home
scope
programme
venue
award
sponsors and organizers
photo gallery
participants


The lectures in pdf format and all additional materials can be found here.





March 3rd  - Monday

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

March 4th - Tuesday

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

March 5th - Wednesday

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

March 6th - Thursday

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

March 7th - Friday

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

March 8th - Saturday

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ă

March 9th - Sunday


Free discussions

March 10th - Monday

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