Abstract is missing.
- The Rodin Platform Has Turned TenLaurent Voisin, Jean-Raymond Abrial. 1-8 [doi]
- Development of a Verified Flash File SystemGerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Dominik Haneberg, Wolfgang Reif. 9-24 [doi]
- Why Amazon Chose TLA +Chris Newcombe. 25-39 [doi]
- Translating B to TLA + for Validation with TLCDominik Hansen, Michael Leuschel. 40-55 [doi]
- αRby - An Embedding of Alloy in RubyAleksandar Milicevic, Ido Efrati, Daniel Jackson. 56-71 [doi]
- MAZE: An Extension of Object-Z for Multi-Agent SystemsGraeme Smith, Qin Li. 72-85 [doi]
- Quasi-Lexicographic ConvergenceStefan Hallerstede. 86-100 [doi]
- Towards B as a High-Level Constraint Modelling Language - Solving the Jobs Puzzle ChallengeMichael Leuschel, David Schneider. 101-116 [doi]
- Analysis of Self-⋆ and P2P Systems Using RefinementManamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh. 117-123 [doi]
- B Formal Validation of ERTMS/ETCS Railway Operating RulesRahma Ben Ayed, Simon Collart Dutilleul, Philippe Bon, Akram Idani, Yves Ledru. 124-129 [doi]
- Modelling Energy Consumption in Embedded Systems with VDM-RTJosé Antonio Esparza Isasa, Peter Würtz Vinther Jørgensen, Claus Ballegård Nielsen, Stefan Hallerstede. 130-135 [doi]
- Sealed Containers in ZEerke A. Boiten, Jeremy Jacob. 136-141 [doi]
- Specifying Transaction Control to Serialize Concurrent Program ExecutionsEgon Börger, Klaus-Dieter Schewe. 142-157 [doi]
- Distributed Situation Analysis - A Formal Semantic FrameworkNarek Nalbandyan, Uwe Glässer, Hamed Yaghoubi Shahir, Hans Wehn. 158-173 [doi]
- Introducing Aspect-Oriented Specification for Abstract State MachinesMarcel Dausend, Alexander Raschke. 174-187 [doi]
- Modular Refinement for Submachines of ASMsGidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif. 188-203 [doi]
- Towards ASM-Based Formal Specification of Self-Adaptive SystemsElvinia Riccobene, Patrizia Scandurra. 204-209 [doi]
- Distributed ASM - Pitfalls and SolutionsAndreas Prinz, Edel Sherratt. 210-215 [doi]
- WebASM: An Abstract State Machine Execution Environment for the WebSimone Zenzaro, Vincenzo Gervasi, Jacopo Soldani. 216-221 [doi]
- Formal System Modelling Using Abstract Data Types in Event-BAndreas Fürst, Thai Son Hoang, David A. Basin, Naoto Sato, Kunihiko Miyazaki. 222-237 [doi]
- Formal Derivation of Distributed MapReduceInna Pereverzeva, Michael Butler, Asieh Salehi Fathabadi, Linas Laibinis, Elena Troubitsyna. 238-254 [doi]
- Validating the RBAC ANSI 2012 Standard Using BNghi Huynh, Marc Frappier, Amel Mammar, Régine Laleau, Jules Desharnais. 255-270 [doi]
- Invariant Guided System DecompositionRichard Banach. 271-276 [doi]
- Understanding and Planning Event-B Refinement through Primitive RationalesTsutomu Kobayashi, Fuyuki Ishikawa, Shinichi Honiden. 277-283 [doi]
- Templates for Event-B Code GenerationAndrew Edmunds. 284-289 [doi]
- The BWare Project: Building a Proof Platform for the Automated Verification of B Proof ObligationsDavid Delahaye, Catherine Dubois, Claude Marché, David Mentré. 290-293 [doi]
- Tuning the Alt-Ergo SMT Solver for B Proof ObligationsSylvain Conchon, Mohamed Iguernelala. 294-297 [doi]
- Fixed-Point Arithmetic Modeled in B Software Using RealsJérôme Guéry, Olivier Rolland, Joris Rehm. 298-302 [doi]
- Bounded Model Checking of Temporal Formulas with AlloyAlcino Cunha. 303-308 [doi]
- Formal Verification of OS Security Model with Alloy and Event-BPetr N. Devyanin, Alexey V. Khoroshilov, Victor V. Kuliamin, Alexander K. Petrenko, Ilya V. Shchepetkov. 309-313 [doi]
- Detecting Network Policy Conflicts Using AlloyFerney A. Maldonado-Lopez, Jaime Chavarriaga, Yezid Donoso. 314-317 [doi]
- Staged Evaluation of Partial Instances in a Relational Model FinderVajih Montaghami, Derek Rayside. 318-323 [doi]
- Domain-Specific Visualization of Alloy InstancesLoïc Gammaitoni, Pierre Kelsen. 324-327 [doi]
- Optimizing Alloy for Multi-objective Software Product Line ConfigurationEd Zulkoski, Chris Kleynhans, Ming-Ho Yee, Derek Rayside, Krzysztof Czarnecki. 328-333 [doi]