May 20 (in Dan David Bld. room 110)
- 9:30 Opening Greetings
- 10:10-11:00 Anatol Slissenko, University
Paris 12, Predicate Logic
Framework for Verification of Timed
Distributed Systems,
- 11;10-12:00
David Harel, Weizmann
A Grand Challenge for Computing: Full Reactive Modeling of a
Multi-Cellular Animal
- 12:00-14:00 LUNCH
- 14:10-15:00
Boaz Trakhtenbrot, Tel Aviv University Understanding Circuits and Hybrid AUtomata.
- 15:10-16:00
Eugene Asarin (VERIMAG)
Verification of hybrid and continuous systems: results and
problems
-
16:00-16:30 Break
- 16:30-17:20 Amir Pnueli, Weizmann,
Translation Validation of Optimizing Compilers
- 17:30-18:30 Discussions: Models for Real time Systems
- Panel:
Oded Maler, Alex Rabinovich, Anatol Slissenko, Boaz Trakhtenbrot
May 21 (in Dan David Bld. room 110)
- 9:10-10:00 Mike Gordon, Cambridge Executing the formal semantics of
the Accellera Property Specification Language by mechanised
theorem proving
- 10:00-10:30 Gila Gohen and Orna Kupferman HU,
Incremental LTL model checking
- 10:30-11:00
Break
-
11:00-11:50
Yoram Hirshfeld,Tel Aviv University
Temporal Logic For Real Time Computations
- 11:50-12:20 Gideon Ariely, Ministry of
Science Unifying theory for
operational and denotational semantics.
- 12:20-14:10 Lunch
- 14:10-15:00 Philippe Schnoebelen, Laboratory for Specification and Verification, ENS Cachan
Model checking
branching-time temporal logics"
- 15:00-15:30
Cindy Eisner, IBM HRL
Reasoning About Multiply-Clocked Hardware
- 15:30- 16:00 Break
- 16:00-16:50
Daniele Beauquier, Paris 12
Decidable properties for monadic Abstract State Machines (ASMs)
- 16:50-17:40
Discussion: Comparison of various
approaches to verification
- Panel: Nachum Dershowitz, Cindy Eisner,
Mike Gordon, Mooly Sagiv
May 22 (in Rozenblat auditorium)