| Time |
Paper Title |
Authors |
| 14:00 |
CSP + clocks: a process algebra for timed automata |
S. Cattani et al. |
| 14:30 |
Projection onto state in the duration calculus: relative completeness |
D. Guelev et al. |
| 14:50 |
CSP model checking of liveness properties over eventual delivery networks |
W. Simmonds |
| 15:10 |
A First Glimpse at Patterns of Data-Independent Induction |
M. Goldsmith et al. |
| 15:30 |
Break |
- |
| 16:00 |
On the expressiveness of CSP refinement checking |
B. Roscoe |
| 16:30 |
Automatic verification of real time systems: a case study |
E. Prokofieva et al. |
| 16:50 |
Compositional CSL model checking for boucherie product processes |
P. Ballarini et al. |
| 17:10 |
A hoare logic for single-input single-output continuous-time control systems |
U. Martin et al. |
| 17:30 |
Break |
- |
| 18:00 |
Model Checking Competition |
- |
| 20:00 |
Conference Dinner |
- |
Persons interested to participate in the model checking competition should
bring their own laptop along.
You can either participate with your own tool, or use some other tool (Spin, SMV,
FDR,...).
We will try to make the model checking task fair, and give scope for various
formalisms to excel.
| Time |
Paper Title |
Authors |
| 13:30 |
Deductive verification of cache coherence protocols |
A. Lisitsa et al. |
| 14:00 |
Modelling ad hoc on-demand distance vector protocol with timed automata |
S. Chiyangwa et al. |
| 14:20 |
Modelling ad-hoc routing protocols using game search |
I. Zakiuddin et al. |
| 14:40 |
Using probabilistic model checking for dynamic power management |
G. Norman et al. |
| 15:00 |
Break |
- |
| 15:30 |
An experiment on synthesis and verification of an industrial process control in
the DSL environment |
T. Massart et al. |
| 16:00 |
Model checking Rebeca code by SMV |
M. Sirjani et al. |
| 16:20 |
Feature Integration from a theory change perspective |
H. Harris et al. |
| 16:40 |
Using the extensible model checker XTL to verify StAC business specifications |
J.-C. Augusto et al. |
| 17:00 |
Close |
- |