Table of Contents

• A Structure for Dependability ArgumentsDaniel Jackson, Eunsuk Kang. 1 [doi]
• Formal Probabilistic Analysis: A Higher-Order Logic Based ApproachOsman Hasan, Sofiène Tahar. 2-19 [doi]
• Synchronous Message Passing and Semaphores: An Equivalence ProofIain Craig, Egon Börger. 20-33 [doi]
• AsmL-Based Concurrency Semantic Variations for Timed Use Case MapsJameleddine Hassine. 34-46 [doi]
• Bârun: A Scripting Language for CoreASMMichael Altenhofen, Roozbeh Farahbod. 47-60 [doi]
• AsmetaSMV: A Way to Link High-Level ASM Models to Low-Level NuSMV SpecificationsPaolo Arcaini, Angelo Gargantini, Elvinia Riccobene. 61-74 [doi]
• An Executable Semantics of the SystemC UML ProfileElvinia Riccobene, Patrizia Scandurra. 75-90 [doi]
• Specifying Self-configurable Component-Based Systems with FracToyAlban Tiberghien, Philippe Merle, Lionel Seinturier. 91-104 [doi]
• Trace Specifications in AlloyJeremy L. Jacob. 105-117 [doi]
• An Imperative Extension to AlloyJoseph P. Near, Daniel Jackson. 118-131 [doi]
• Towards Formalizing Network Architectural DescriptionsJoud Khoury, Chaouki T. Abdallah, Gregory L. Heileman. 132-145 [doi]
• Lightweight Modeling of Java Virtual Machine Security ConstraintsMark C. Reynolds. 146-159 [doi]
• Alloy+HotCore: A Fast Approximation to Unsat CoreNicolás D Ippolito, Marcelo F. Frias, Juan P. Galeotti, Esteban Lanzarotti, Sergio Mera. 160-173 [doi]
• Supporting Reuse in Event B Development: Modularisation ApproachAlexei Iliasov, Elena Troubitsyna, Linas Laibinis, Alexander Romanovsky, Kimmo Varpaaniemi, Dubravka Ilic, Timo Latvala. 174-188 [doi]
• Reasoned Modelling Critics: Turning Failed Proofs into Modelling GuidanceAndrew Ireland, Gudmund Grov, Michael Butler. 189-202 [doi]
• Applying the B Method for the Rigorous Development of Smart Card ApplicationsBruno Emerson Gurgel Gomes, David Déharbe, Anamaria Martins Moreira, Katia Moraes. 203-216 [doi]
• Automatic Verification for a Class of Proof Obligations with SMT-SolversDavid Déharbe. 217-230 [doi]
• A Refinement-Based Correctness Proof of Symmetry Reduced Model CheckingEdd Turner, Michael Butler, Michael Leuschel. 231-244 [doi]
• Development of a Synchronous Subset of AADLMamoun Filali-Amine, Julia L. Lawall. 245-258 [doi]
• Matelas: A Predicate Calculus Common Formal Definition for Social NetworkingNéstor Cataño, Camilo Rueda. 259-272 [doi]
• Structured Event-B Models and ProofsStefan Hallerstede. 273-286 [doi]
• Refinement-Animation for Event-B - Towards a Method of ValidationStefan Hallerstede, Michael Leuschel, Daniel Plagge. 287-301 [doi]
• Reactivising Classical BSteve Dunne, Frank Zeyda. 302-318 [doi]
• Event-B Decomposition for Parallel ProgramsThai Son Hoang, Jean-Raymond Abrial. 319-333 [doi]
• Communication Systems in ClawZMichael Vernon, Frank Zeyda, Ana Cavalcanti. 334-348 [doi]
• Formalising and Validating RBAC-to-XACML Translation Using Lightweight Formal MethodsMark Slaymaker, David J. Power, Andrew Simpson. 349-362 [doi]
• Towards Formally Templated Relational Database Representations in ZNicolas Wu, Andrew Simpson. 363-376 [doi]
• Translating Z to AlloyPetra Malik, Lindsay Groves, Clare Lenihan. 377-390 [doi]
• B-ASM: Specification of ASM à la BDavid Michel, Frédéric Gervais, Pierre Valarcher. 391 [doi]
• A Case for Using Data-Flow Analysis to Optimize Incremental Scope-Bounded CheckingDanhua Shao, Divya Gopinath, Sarfraz Khurshid, Dewayne E. Perry. 392-393 [doi]
• On the Modelling and Analysis of Amazon Web Services Access PoliciesDavid J. Power, Mark Slaymaker, Andrew Simpson. 394 [doi]
• Architecture as an Independent Variable for Aspect-Oriented Application DescriptionsHamid Bagheri, Kevin J. Sullivan. 395 [doi]
• ParAlloy: Towards a Framework for Efficient Parallel Analysis of Alloy ModelsNicolás Rosner, Juan P. Galeotti, Carlos López Pombo, Marcelo F. Frias. 396-397 [doi]
• Introducing Specification-Based Data Structure Repair Using AlloyRazieh Nokhbeh Zaeem, Sarfraz Khurshid. 398-399 [doi]
• Secrecy UML Method for Model TransformationsWaël Hassan, Nadera Slimani, Kamel Adi, Luigi Logrippo. 400 [doi]
• Improving Traceability between KAOS Requirements Models and B SpecificationsAbderrahman Matoussi, Dorian Petit. 401-402 [doi]
• Code Synthesis for Timed Automata: A Comparison Using Case StudyAnaheed Ayoub, Ayman M. Wahba, Ashraf M. Salem, Mohamed A. Sheirah. 403 [doi]
• Towards Validation of Requirements ModelsAtif Mashkoor, Abderrahman Matoussi. 404 [doi]
• A Proof Based Approach for Formal Verification of Transactional BPEL Web ServicesIdir Aït-Sadoune, Yamine Aït Ameur. 405-406 [doi]
• On an Extensible Rule-Based Prover for Event-BIssam Maamria, Michael Butler, Andrew Edmunds, Abdolbaghi Rezazadeh. 407 [doi]
• B Model Abstraction Combining Syntactic and Semantic MethodsJacques Julliand, Nicolas Stouls, Pierre-Christope Bué, Pierre-Alain Masson. 408 [doi]
• A Basis for Feature-Oriented Modelling in Event-BJennifer Sorge, Michael Poppleton, Michael Butler. 409 [doi]
• Using Event-B to Verify the Kmelia Components and Their AssembliesPascal André, Gilles Ardourel, Christian Attiogbé, Arnaud Lanoix. 410 [doi]
• Starting B Specifications from Use CasesThiago C. de Sousa, Aryldo G. Russo. 411 [doi]
• Integrating SMT-Solvers in Z and B ToolsAlessandro Cavalcante Gurgel, Valério Gutemberg de Medeiros, Marcel Vinicius Medeiros Oliveira, David Boris Paul Déharbe. 412-413 [doi]
• Formal Analysis in Model Management: Exploiting the Power of CZTJames R. Williams, Fiona A. C. Polack, Richard F. Paige. 414 [doi]