<html>
****************************************************************************<br>
Our apologies for the inconvenience if you receive multiple copies <br>
****************************************************************************<br>
<br>
<b>Registration - Register you for B2007 - Registration<br>
<br>
</b>The B 2007 conference will take place in Besançon, France <br>
on 17-19 Janauary 2007.<br>
<br>
The program for the B 2007 conference is now complete: <br>
<font size=2><a href="http://lifc.univ-fcomte.fr/b2007/pages/programme.htm" eudora="autourl">http://lifc.univ-fcomte.fr/b2007/pages/programme.</a><a href="http://lifc.univ-fcomte.fr/b2007/pages/programme.htm" eudora="autourl">htm<br>
</a></font>Also, you will find it hereunder.<br>
<br>
If you are interested in attending the conference, you can <br>
register on-line. The registration page can be found at <br>
<font size=2><a href="http://lifc.univ-fcomte.fr/b2007/pages/registration.htm" eudora="autourl">http://lifc.univ-fcomte.fr/b2007/pages/registration.</a><a href="http://lifc.univ-fcomte.fr/b2007/pages/registration.htm" eudora="autourl">htm<br>
<br>
</a></font>Registration fees amount to 350 euros until December 1st 2006,
and <br>
450 euros after. Fees<font size=2> include admission to conference,
proceedings,</font> <br>
<font size=2>3 lunches and conference banquet.<br>
<br>
Best regards.<br>
</font><tt>Jacques Julliand<br>
<br>
<br>
</tt><div align="center">
<font face="Courier New, Courier" size=5><b>B 2007
</font><font face="Arial Black, Helvetica" size=6>Conference
Program<br>
<br>
<br>
</font></div>
Wednesday 17 January<br>
<x-tab> </x-tab></b>9h<x-tab> </x-tab><x-tab> </x-tab><b>Registration<br>
</b><x-tab> </x-tab>9h45<x-tab> </x-tab><x-tab> </x-tab><b>Welcome
Opening<br>
</b><x-tab> </x-tab>10h<x-tab> </x-tab><x-tab> </x-tab><b>Invited
talk by</b> Joseph Morris, School of computing,<br>
<x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab>Dublin
city university, Ireland Plug and Play Nondeterminacy<br>
<x-tab> </x-tab><br>
<x-tab> </x-tab>11h<x-tab> </x-tab><x-tab> </x-tab><b>Coffee
break<br>
</b><x-tab> </x-tab>11h30<x-tab> </x-tab><x-tab> </x-tab><b>Session:
Theoretical issues</b>
<dl>
<dl>
<dl>
<dd>- Interpreting Invariant Composition in the B Method Using Spec#
</dl>
</dl>
</dl><x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab>ownership
relation : a way to explain and relax B restrictions<br>
<x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab>Sylvain
Boulmé and Marie-Laure Potet, U. of Grenoble - France
<dl>
<dl>
<dl>
<dd>- Chorus Angelorum
</dl>
</dl>
</dl><x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab>Steve
Dunne, U. of Teesside UK<br>
<x-tab> </x-tab>12h30<x-tab> </x-tab><x-tab> </x-tab><b>Presentation
of tool exhibitions by</b> Fabrice Bouquet<br>
<x-tab> </x-tab>12h45<x-tab> </x-tab><x-tab> </x-tab><b>Tool
session:</b> <br>
<x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab>-
A JAG Extension for Verifying LTL Properties on B Event Systems<br>
<x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab>Julien
Groslambert, U. of Franche-Comté - France<br>
<x-tab> </x-tab>13h<x-tab> </x-tab><x-tab> </x-tab><b>Lunch<br>
</b><x-tab> </x-tab>14h30<x-tab> </x-tab><x-tab> </x-tab><b>Session:
B extensions<br>
</b><x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab>-
Augmenting B with Control Annotations<br>
<x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab>Wilson
Ifill, Steve Schneider and Helen Treharne, U. of Surrey UK
<dl>
<dl>
<dl>
<dd>- Justifications for the Event-B Modelling Notation
<dd>Stefan Hallerstede, ETH Zürich - Switzerland
</dl>
</dl>
</dl><x-tab> </x-tab>15h30<x-tab> </x-tab><x-tab> </x-tab><b>Tool
session:</b>
<dl>
<dl>
<dl>
<dd>- A Generic Flash-based Animation Engine for ProB
<dd>Jens Bendisposto and Michael Leuschel, U. of Düsseldorf, Germany
<dd>- An Extensible Smart Editor for B in Eclipse
<dd>Jens Bendisposto and Michael Leuschel, U. of Düsseldorf, Germany
</dl>
</dl>
</dl><x-tab> </x-tab>16h<x-tab> </x-tab><x-tab> </x-tab><b>Coffee
break and Demos<br>
</b><x-tab> </x-tab>16h30<x-tab> </x-tab><b>Session:
B Tools, tests and model-checking<br>
<x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab></b>-<b>
</b>Automatic Translation from Combined B and CSP Specification to<br>
<x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab>Java Programs<br>
<b><x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab></b>Letu Yang UK, Michael Poppleton, U.of Southampton UK
<dl>
<dl>
<dl>
<dd>- Symmetry Reduction for B by Permutations Flooding
<dd>Michael Leuschel and Corinna Spermann, U. of Düsseldorf Germany
<dd>Michael Butler and Edward Turner, U.of Southampton UK
<dd>- Instantiation of Parameterized Data Structures for Model-Based Testing
<dd>Fabrice Bouquet, Jean-François Couchot, Frédéric Dadeau and Alain
<dd>Giorgetti, U. of Franche-Comté France
</dl>
</dl>
</dl><x-tab> </x-tab>18h<x-tab> </x-tab><x-tab> </x-tab><b>End of session<br>
</b><x-tab> </x-tab>18h30<x-tab> </x-tab><x-tab> </x-tab><b>Reception in the town hall<br>
</b><x-tab> </x-tab><br>
<br>
<br>
<b>Thursday 18 January<br>
<x-tab> </x-tab></b>9h<x-tab> </x-tab><x-tab> </x-tab><b>Invited talk by</b> Leslie Lamport, Microsoft corporation
<dl>
<dl>
<dd><x-tab> </x-tab><x-tab> </x-tab>- Comparing TLA+ and B
</dl>
</dl><x-tab> </x-tab>10h<x-tab> </x-tab><x-tab> </x-tab><b>Session: B extension</b>
<dl>
<dl>
<dl>
<dd>- Verification of LTL Properties in B Event Systems
<dd>Julien Groslambert, U. of Franche-Comté - France
</dl>
</dl>
</dl><x-tab> </x-tab>10h30<x-tab> </x-tab><x-tab> </x-tab><b>Coffee break and Demos <br>
</b><x-tab> </x-tab>11h<x-tab> </x-tab><x-tab> </x-tab><b>Session: Case studies and specification method<br>
<x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab></b>-<b> </b>Design<b> </b>Patterns for B: Bridging Formal and Informal Development<br>
<x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab>Edward Chan, Ken Robinson and Brett Welch, U. of New South Wales
<dl>
<dl>
<dd> Australia
<dl>
<dd>- Time Constraint Patterns in Event B Development
<dd>Dominique Cansell, Dominique Méry, Joris Rehm, U. of Nancy France
<dd>- Modelling and Proof Analysis of Interrupt Driven Scheduling
<dd>Bill Stoddard and Frank Zeyda, U. of Teesside UK
<dd>Dominique Cansell, U. of Metz France
</dl>
</dl>
</dl><x-tab> </x-tab>12h30<x-tab> </x-tab><x-tab> </x-tab><b>Lunch <br>
</b><x-tab> </x-tab><br>
<x-tab> </x-tab>14h<x-tab> </x-tab><x-tab> </x-tab><b>Industrial</b> <b>event: Invited talk by</b> Eddie Jaffuel,<br>
<x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab>Leirios Technologie - France<br>
<x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab>Using B Abstract Machine for Model-Based Testing of Smartcard Software<br>
<br>
<x-tab> </x-tab>15h<x-tab> </x-tab><x-tab> </x-tab><b>Session:</b> <b>Industrial experiences</b>
<dl>
<dl>
<dl>
<dd>-Experiences in Using B and UML in Industrial Development
<dd>Ian Oliver, Nokia Research Center - Finland
<dd>- B in large-Scale Projects : The Canarsie Line CBTC Experience
<dd>Daniel Dollé, Didier Essamé, SIEMENS Transportation Systems - France
</dl>
</dl>
</dl><x-tab> </x-tab>16h<x-tab> </x-tab><x-tab> </x-tab><b>Coffee break and Demos<br>
</b><x-tab> </x-tab>16h30<x-tab> </x-tab><b>Session: Industrial experiences<br>
<x-tab> </x-tab><x-tab> </x-tab></b>- A Tool for Firewall Administration<br>
<x-tab> </x-tab><x-tab> </x-tab>Mathieu Clabaut, Systerel France<br>
<x-tab> </x-tab><x-tab> </x-tab>- The B-Method for the Construction of Microkernel-Based Systems<br>
<x-tab> </x-tab><x-tab> </x-tab>Sarah Hoffmann and Sophie Gabriele, STMicroelectronics - France
<dl>
<dl>
<dl>
<dd>-Hardware Verification and Beyond : Using B at AWE
<dd>Neils Evans and Wilson Ifill, Atomic Weapons Establishment - UK
</dl>
</dl>
</dl><x-tab> </x-tab>18h<x-tab> </x-tab><x-tab> </x-tab><b>End of Industrial Event<br>
</b><x-tab> </x-tab>18h30<x-tab> </x-tab><x-tab> </x-tab><b>Visit of Time Muséum<br>
<x-tab> </x-tab></b>20h <x-tab> </x-tab><x-tab> </x-tab><b>Conference dinner<br>
<br>
<br>
<br>
Friday 19 January<br>
<x-tab> </x-tab></b>9h<x-tab> </x-tab><x-tab> </x-tab><b>Invited talk by</b> Chemouil, CNES, Toulouse,<br>
<x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab>The Design of Spacecraft Flight Software<br>
<x-tab> </x-tab><br>
<x-tab> </x-tab>10h<x-tab> </x-tab><x-tab> </x-tab><b>Industrial</b> <b>Tool session </b>
<dl>
<dl>
<dl>
<dd>- BRAMA : a New Graphic Animation Tool for B Models
<dd>Clearsy - France
<dd>- LEIRIOS Test Generator : Automated test Generation From B models
<dd>Eddie Jaffuel and Bruno Legeard, LEIRIOS Technologies - France
</dl>
</dl>
</dl><x-tab> </x-tab>10h45<x-tab> </x-tab><x-tab> </x-tab><b>Coffee break <br>
</b><x-tab> </x-tab>11h15<x-tab> </x-tab><x-tab> </x-tab><b>Session : Integration and Derivation</b>
<dl>
<dl>
<dl>
<dd>- Refinement of Statemachines using Event B semantics
<dd>Colin Snook, U. Of Southampton UK and Marina Waldén, U. of Turku Finland
<dd>- Formal Transformation of Platform Independent Models into Platform
<dd>Pontus Boström, Mats Neovius, Marina Waldén, U. of Turku and , Ian Oliver, NOKIA Finland
<dd>- Refinement of EB3 Process Patterns into B Specifications
<dd>Frederic Gervais, CNAM-IIE, Regine Laleau, U. of Paris 12 France
<dd>Marc Frappier, U. of Sherbrooke Canada
</dl>
</dl>
</dl><x-tab> </x-tab>12h15<x-tab> </x-tab><x-tab> </x-tab><b>Demo<br>
</b><x-tab> </x-tab><br>
<x-tab> </x-tab>12h30<x-tab> </x-tab><x-tab> </x-tab><b>Lunch<br>
<x-tab> </x-tab></b>14H00<x-tab> </x-tab><x-tab> </x-tab><b>Invited talk by </b>Paul Gibson, National University of Ireland,<br>
<x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab>Maynooth<br>
<x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab>- The need for rigourous software engineering -<br>
<x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab> the past, present and future <br>
<br>
<x-tab> </x-tab>15h00<x-tab> </x-tab><x-tab> </x-tab><b>Tool session </b>
<dl>
<dl>
<dl>
<dd>- JML2B : Checking JML specifications with B machines
<dd>Fabrice Bouquet, Frédéric Dadeau and Julien Groslambert, U. of Franche-Comté - France
</dl>
</dl>
</dl><b><x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab></b>-<b> </b>Meca : a tool for access control models<br>
<x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab>Amal Haddad, U. of Grenoble - France<br>
<b><x-tab> </x-tab><x-tab> </x-tab><x-tab> </x-tab><br>
</b><x-tab> </x-tab>15h30<x-tab> </x-tab><x-tab> </x-tab><b>Session : Security policy verification</b>
<dl>
<dl>
<dl>
<dd>- Security policy enforcement through refinement process
<dd>Nicolas Stouls, Marie-Laure Potet, U. of Grenoble France
<dd>- Integration of security policy into event B modeling
<dd>Nazim Benaissa, Dominique Cansell and Dominique Méry, U. of Nancy France
</dl>
</dl>
</dl><x-tab> </x-tab>16h30<x-tab> </x-tab><x-tab> </x-tab><b>Closing session<br>
<br>
</b><x-tab> </x-tab>17h<x-tab> </x-tab><x-tab> </x-tab><b>End of the Conference<br>
<br>
</b><x-sigsep><p></x-sigsep>
Bien sincèrement.<br>
<br>
Jacques Julliand<br>
---------------------------------------------------------------<br>
Directeur du Laboratoire d'Informatique de l'<br>
Université de Franche-Comté<br>
LIFC (FRE CNRS 2661)<br>
---------------------------------------------------------------<br>
16, route de Gray<br>
25030 Besançon Cedex<br>
<br>
tel : (33) 03.81.66.64.51<br>
secrétariat : 03.81.66.64.55 (ou 65.15), Fax : 64.50<br>
<br>
E-mail : jacques.julliand@lifc.univ-fcomte.fr<br>
Web : <a href="http://lifc.univ-fcomte.fr/" eudora="autourl">http://</a>lifc.univ-fcomte<a href="http://lifc.univ-fcomte.fr/" eudora="autourl">.fr</a><br>
---------------------------------------------------------------<br>
<br>
<br>
<div>Bien sincèrement.</div>
<br>
<div> Jacques Julliand</div>
<div>---------------------------------------------------------------</div>
<div>Directeur du Laboratoire d'Informatique de l'</div>
<div>Université de Franche-Comté</div>
<div>LIFC (FRE CNRS 2661)</div>
<div>---------------------------------------------------------------</div>
<div>16, route de Gray</div>
<div>25030 Besançon Cedex</div>
<br>
<div>tel : (33) 03.81.66.64.51</div>
<div>secrétariat : 03.81.66.64.55 (ou 65.15), Fax : 64.50</div>
<br>
<div>E-mail : jacques.julliand@lifc.univ-fcomte.fr</div>
<div>Web : <a href="http://lifc.univ-fcomte.fr/" EUDORA=AUTOURL>http://lifc.univ-fcomte.fr</a></div>
<div>---------------------------------------------------------------</div>
<br>
</html>