Abstract is missing.
- E-Voting and the Need for Rigourous Software Engineering - The Past, Present and FutureJ. Paul Gibson. 1 [doi]
- Using B Machines for Model-Based Testing of Smartcard SoftwareEddie Jaffuel. 2 [doi]
- The Design of Spacecraft On-Board SoftwareDavid Chemouil. 3 [doi]
- Interpreting Invariant Composition in the B Method Using the Spec# Ownership Relation: A Way to Explain and Relax B RestrictionsSylvain Boulmé, Marie-Laure Potet. 4-18 [doi]
- Chorus AngelorumSteve Dunne. 19-33 [doi]
- Augmenting B with Control AnnotationsWilson Ifill, Steve A. Schneider, Helen Treharne. 34-48 [doi]
- Justifications for the Event-B Modelling NotationStefan Hallerstede. 49-63 [doi]
- Automatic Translation from Combined ::::B:::: and CSP Specification to Java ProgramsLetu Yang, Michael Poppleton. 64-78 [doi]
- Symmetry Reduction for B by Permutation FloodingMichael Leuschel, Michael J. Butler, Corinna Spermann, Edd Turner. 79-93 [doi]
- Instantiation of Parameterized Data Structures for Model-Based TestingFabrice Bouquet, Jean-Francois Couchot, Frédéric Dadeau, Alain Giorgetti. 94-108 [doi]
- Verification of LTL on B Event SystemsJulien Groslambert. 109-124 [doi]
- Patterns for B: Bridging Formal and Informal DevelopmentEdward Chan, Ken Robinson, Brett Welch. 125-139 [doi]
- Time Constraint Patterns for Event B DevelopmentDominique Cansell, Dominique Méry, Joris Rehm. 140-154 [doi]
- Modelling and Proof Analysis of Interrupt Driven SchedulingBill Stoddart, Dominique Cansell, Frank Zeyda. 155-170 [doi]
- Refinement of Statemachines Using Event B SemanticsColin F. Snook, Marina A. Waldén. 171-185 [doi]
- Formal Transformation of Platform Independent Models into Platform Specific ModelsPontus Boström, Mats Neovius, Ian Oliver, Marina A. Waldén. 186-200 [doi]
- Refinement of eb:::3::: Process Patterns into B SpecificationsFrédéric Gervais, Marc Frappier, Régine Laleau. 201-215 [doi]
- Security Policy Enforcement Through Refinement ProcessNicolas Stouls, Marie-Laure Potet. 216-231 [doi]
- Integration of Security Policy into System ModelingNazim Benaïssa, Dominique Cansell, Dominique Méry. 232-247 [doi]
- Experiences in Using B and UML in Industrial DevelopmentIan Oliver. 248-251 [doi]
- B in Large-Scale Projects: The Canarsie Line CBTC ExperienceDidier Essamé, Daniel Dollé. 252-254 [doi]
- A Tool for Firewall AdministrationMathieu Clabaut. 255-256 [doi]
- The B-Method for the Construction of Microkernel-Based SystemsSarah Hoffmann, Germain Haugou, Sophie Gabriele, Lilian Burdy. 257-259 [doi]
- Hardware Verification and Beyond: Using B at AWENeil Evans, Wilson Ifill. 260-261 [doi]
- AJulien Groslambert. 262-265 [doi]
- A Generic Flash-Based Animation Engine for ProBJens Bendisposto, Michael Leuschel. 266-269 [doi]
- BE:::4:::: The B Extensible Eclipse Editing EnvironmentJens Bendisposto, Michael Leuschel. 270-273 [doi]
- BRAMA: A New Graphic Animation Tool for B ModelsThierry Servat. 274-276 [doi]
- LEIRIOS Test Generator: Automated Test Generation from B ModelsEddie Jaffuel, Bruno Legeard. 277-280 [doi]
- Meca: A Tool for Access Control ModelsAmal Haddad. 281-284 [doi]
- JML2B: Checking JML Specifications with B MachinesFabrice Bouquet, Frédéric Dadeau, Julien Groslambert. 285-288 [doi]
- Plug-and-Play NondeterminacyJoseph M. Morris. 289-292 [doi]