Programme of AVoCS and Rodin User and Developer Workshop 2010 | ||||
Room 2B | Room 2C | |||
Monday, Sept. 20 | ||||
Rodin Tutorial Day | ||||
9:00 | Creating a Plug-in | |||
Extending the Database | ||||
Extending the Structured Editor | ||||
10:30 | Coffee Break | |||
11:00 | Extending the Pretty Print Page | |||
Providing Help | ||||
Extending the Event-B Explorer | ||||
12:30 | Lunch | |||
14:00 | Extending the Static Checker | |||
Extending the Proof Obligation Generator | ||||
15:30 | Coffee Break | |||
16:00 | Adding Reasoners | |||
17:00 | ||||
Tuesday, Sept. 21 | ||||
Rodin User and Developer Workshop | ||||
09:00 | Atomicity Decomposition a Technique for Structuring Refinement in Event-B | |||
Asieh Salehi Fathabadi, Michael Butler | ||||
09:30 | Integrating astd in the Rodin platform | |||
Paul Amar, Marc Frappier, Cecile Lartaud, Jeremy Milhau | ||||
10:00 | Potpourri of what? One year in a DA's life | |||
Aryldo G. Russo Jr., Thiago C. de Sousa, Haniel Barbosa, Paulo Muniz, David Deharbe | ||||
10:30 | Coffee break | |||
11:00 | The ProR Requirements Engineering Platform | |||
Michael Jastram | ||||
11:30 | A Refinement Planning Sheet | |||
Shin Nakajima | ||||
12:00 | Refinement Plans for Reasoned Modelling | |||
Maria Teresa Llano, Andrew Ireland, Gudmund Grov | ||||
12:30 | Lunch | |||
13:45 | AVOCS Opening | |||
14:00 | Specification of the Automatic Prover P3 | |||
Jean-Raymond Abrial, Dominique Cansell, Christophe Metayer | ||||
AVoCS | Rodin User and Developer Workshop | |||
15:00 | Static Analysis of Information Release in Interactive Programs | 15:00 | Reflections on the teaching of System Modelling and Design | |
Adedayo Adetoye, Nikolaos Papanikolaou | Ken Robinson | |||
15:30 | Coffee Break | 15:30 | Coffee Break | |
AVoCS | Rodin User and Developer Workshop | |||
16:00 | Confidentiality Certification of source Java code in JavaPCC | 16:00 | Verification of a Byzantine Agreement Protocol using Event-B | |
Mauricio Alba-Castro, Maria Alpuente, Santiago Escobar. | Roman Krenicky, Mattias Ulbrich | |||
16:20 | Model Checking the Pastry Routing Protocol | 16:30 | Code Generation with the Event-B Tasking Extension (Tool Development) | |
Tianxiang Lu, Stephan Merz, Christoph Weidenbach. | Andy Edmunds | |||
16:40 | Design-Time Model Checking in Part-Whole Statecharts | 17:00 | Modelling Recursion in Event-B | |
Luca Pazzi, Marco Pradelli, Matteo Interlandi | Stefan Hallerstede | |||
17:00 | Reconstruction and verification of group membership protocols | |||
Muhammad Atif, Sjoerd Cranen, MohammadReza Mousavi | ||||
Wednesday, Sept. 22 | ||||
AVoCS | Rodin User and Developer Workshop | |||
09:00 | A Simple Model of Communication APIs -- Application to Dynamic Partial-order Reduction | 09:00 | Using automated theory formation to discover invariants of Event-B models | |
Cristian Rosa, Stephan Merz, Martin Quinson | Maria Teresa Llano, Andrew Ireland, Alison Pease, Simon Colton, John Charnley | |||
09:30 | Verification of a Symmetry Detection Technique using PVS | 09:30 | Specifying and Solving Constraint Satisfaction Problems in B | |
Shamim Ripon, Alice Miller | Michael Leuschel and Daniel Plagge | |||
10:00 | Automated Support for the Design and Validation of Fault Tolerant Parameterized Systems: a case study | 10:00 | Fault Tolerance View in Event-B Development | |
Francesco Alberti, Silvio Ghilardi, Elena Pagani, Silvio Ranise, Gian Paolo Rossi | Ilya Lopatkin, Alexei Iliasov, Alexander Romanovsky | |||
10:30 | Coffee break | 10:30 | Coffee Break | |
AVoCS | Rodin User and Developer Workshop | |||
11:00 | Development of Rabin Choice Coordination in Event-B | 11:00 | Event-B models of P systems | |
Emre Yilmaz, Thai Son Hoang | Florentin Ipate, Turcanu Adrian | |||
11:30 | Checking Consistency Between Message Choreographies And Their Implementation Models | 11:30 | Records | |
Wei Wei, Andreas Roth, Sebastian Wieczorek, Vitaly Kozyura | Vitaly Savicks, Colin Snook, Michael Butler | |||
12:00 | Proving Distributed Algorithms by Combining Refinement and Local Computations | 11:45 | Decomposition Tool: Development and Usage | |
Dominique Méry, Mohamed Mosbah, Mohamed Tounsi | Renato Silva, Carine Pascal, T.S. Hoang, Michael Butler | |||
12:00 | Sequence Refinement, Modularisation Plugin | |||
Alexei Iliasov | ||||
12:15 | Modelling Views Paradigm Support for Rodin | |||
Alexei Iliasov | ||||
12:30 | Lunch | Lunch | ||
14:00 | Ensuring Consistency between Classifiers and Classes | |||
Joseph Kiniry | ||||
AVoCS | Rodin User and Developer Workshop | |||
15:00 | Evaluation Strategies for Datalog-based Points-To Analyses | 15:00 | A small experiment in Event-B rippling | |
Marco A. Feliú, Christophe Joubert, Fernando Tarín | Gudmund Grov, Alan Bundy, Lucas Dixon | |||
15:30 | Coffee Break | 15:30 | Coffee Break | |
AVoCS | Rodin User and Developer Workshop | |||
16:00 | Towards Reusable Formal Method Tools | 16:00 | Animation of UML-B State-machines | |
Marc Fontaine | Vitaly Savicks, Colin Snook, Michael Butler | |||
16:20 | Compensable Workflows in CSP | 16:30 | Addressing Extensibility Issues in Rodin and Event-B | |
Moritz Kleine | Issam Maamria, Michael Butler | |||
16:40 | Automated Translation of Timed Automata to Tock CSP | |||
Maneesh Khattri, Joel Ouaknine, Bill Roscoe | ||||
17:00 | Verification of Railway Interlockings in Scade | |||
Andrew Lawrence, Monika Seisenberger | ||||
17:20 | ||||
18:00 | Reception | |||
19:00 | Java User Group Düsseldorf: Design by Contract with JML | |||
Joseph Kiniry | ||||
21:00 | After Work Party | |||
Thursday, Sept. 22 | ||||
AVoCS | ||||
09:20 | Formal Analysis of a Programmable Performance-Critical Processor Communication Interface | |||
Suleiman Abu Kharmeh, Kerstin Eder, David May | ||||
09:40 | Extending PROMELA and SPIN for hybrid systems analysis | |||
Laura Panizo, Maria del Mar Gallardo | ||||
10:00 | Integrating Automated and Interactive Theorem Proving in Type Theory | |||
Karim Kanso, Anton Setzer | ||||
10:20 | Coffee break | |||
AVoCS | ||||
11:00 | Integrating Formal Methods with Informal Digital Hardware Development | |||
Neil Evans | ||||
11:30 | A Synchronous Approach to Threaded Program Verification | |||
Kenneth Johnson, Loïc Besnard, Thierry Gautier, Jean-Pierre Talpin | ||||
12:00 | Automatically Verifying Railway Interlockings using SAT-based Model Checking | |||
Phillip James, Markus Roggenbach | ||||
12:30 | AVoCS Closing | |||
12:45 | Lunch | |||