A - BZ 2010: Orford, QC, UK

Invited Talks

• Daniel Jackson, Eunsuk Kang:
  A Structure for Dependability Arguments. 1
  
• Osman Hasan, Sofiène Tahar:
  Formal Probabilistic Analysis: A Higher-Order Logic Based Approach. 2-19
  

ASM Papers

• Iain Craig, Egon Börger:
  Synchronous Message Passing and Semaphores: An Equivalence Proof. 20-33
  
• Jameleddine Hassine:
  AsmL-Based Concurrency Semantic Variations for Timed Use Case Maps. 34-46
  
• Michael Altenhofen, Roozbeh Farahbod:
  Bârun: A Scripting Language for CoreASM. 47-60
  
• Paolo Arcaini, Angelo Gargantini, Elvinia Riccobene:
  AsmetaSMV: A Way to Link High-Level ASM Models to Low-Level NuSMV Specifications. 61-74
  
• Elvinia Riccobene, Patrizia Scandurra:
  An Executable Semantics of the SystemC UML Profile. 75-90
  

Alloy Papers

• Alban Tiberghien, Philippe Merle, Lionel Seinturier:
  Specifying Self-configurable Component-Based Systems with FracToy. 91-104
  
• Jeremy L. Jacob:
  Trace Specifications in Alloy. 105-117
  
• Joseph P. Near, Daniel Jackson:
  An Imperative Extension to Alloy. 118-131
  
• Joud Khoury, Chaouki T. Abdallah, Gregory L. Heileman:
  Towards Formalizing Network Architectural Descriptions. 132-145
  
• Mark C. Reynolds:
  Lightweight Modeling of Java Virtual Machine Security Constraints. 146-159
  
• Nicolás D'Ippolito, Marcelo F. Frias, Juan P. Galeotti, Esteban Lanzarotti, Sergio Mera:
  Alloy+HotCore: A Fast Approximation to Unsat Core. 160-173
  

B Papers

• Alexei Iliasov, Elena Troubitsyna, Linas Laibinis, Alexander Romanovsky, Kimmo Varpaaniemi, Dubravka Ilic, Timo Latvala:
  Supporting Reuse in Event B Development: Modularisation Approach. 174-188
  
• Andrew Ireland, Gudmund Grov, Michael Butler:
  Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance. 189-202
  
• Bruno Emerson Gurgel Gomes, David Déharbe, Anamaria Martins Moreira, Katia Moraes:
  Applying the B Method for the Rigorous Development of Smart Card Applications. 203-216
  
• David Déharbe:
  Automatic Verification for a Class of Proof Obligations with SMT-Solvers. 217-230
  
• Edd Turner, Michael J. Butler, Michael Leuschel:
  A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking. 231-244
  
• Mamoun Filali-Amine, Julia L. Lawall:
  Development of a Synchronous Subset of AADL. 245-258
  
• Néstor Cataño, Camilo Rueda:
  Matelas: A Predicate Calculus Common Formal Definition for Social Networking. 259-272
  
• Stefan Hallerstede:
  Structured Event-B Models and Proofs. 273-286
  
• Stefan Hallerstede, Michael Leuschel, Daniel Plagge:
  Refinement-Animation for Event-B - Towards a Method of Validation. 287-301
  
• Steve Dunne, Frank Zeyda:
  Reactivising Classical B. 302-318
  
• Thai Son Hoang, Jean-Raymond Abrial:
  Event-B Decomposition for Parallel Programs. 319-333
  

Z Papers

• Michael Vernon, Frank Zeyda, Ana Cavalcanti:
  Communication Systems in ClawZ. 334-348
  
• Mark Slaymaker, David J. Power, Andrew Simpson:
  Formalising and Validating RBAC-to-XACML Translation Using Lightweight Formal Methods. 349-362
  
• Nicolas Wu, Andrew Simpson:
  Towards Formally Templated Relational Database Representations in Z. 363-376
  
• Petra Malik, Lindsay Groves, Clare Lenihan:
  Translating Z to Alloy. 377-390
  

ABZ Short Papers (Abstracts)

• David Michel, Frédéric Gervais, Pierre Valarcher:
  B-ASM: Specification of ASM à la B. 391
  
• Danhua Shao, Divya Gopinath, Sarfraz Khurshid, Dewayne E. Perry:
  A Case for Using Data-Flow Analysis to Optimize Incremental Scope-Bounded Checking. 392-393
  
• David J. Power, Mark Slaymaker, Andrew Simpson:
  On the Modelling and Analysis of Amazon Web Services Access Policies. 394
  
• Hamid Bagheri, Kevin J. Sullivan:
  Architecture as an Independent Variable for Aspect-Oriented Application Descriptions. 395
  
• Nicolás Rosner, Juan P. Galeotti, Carlos López Pombo, Marcelo F. Frias:
  ParAlloy: Towards a Framework for Efficient Parallel Analysis of Alloy Models. 396-397
  
• Razieh Nokhbeh Zaeem, Sarfraz Khurshid:
  Introducing Specification-Based Data Structure Repair Using Alloy. 398-399
  
• Waël Hassan, Nadera Slimani, Kamel Adi, Luigi Logrippo:
  Secrecy UML Method for Model Transformations. 400
  
• Abderrahman Matoussi, Dorian Petit:
  Improving Traceability between KAOS Requirements Models and B Specifications. 401-402
  
• Anaheed Ayoub, Ayman M. Wahba, Ashraf M. Salem, Mohamed A. Sheirah:
  Code Synthesis for Timed Automata: A Comparison Using Case Study. 403
  
• Atif Mashkoor, Abderrahman Matoussi:
  Towards Validation of Requirements Models. 404
  
• Idir Aït-Sadoune, Yamine Aït Ameur:
  A Proof Based Approach for Formal Verification of Transactional BPEL Web Services. 405-406
  
• Issam Maamria, Michael Butler, Andrew Edmunds, Abdolbaghi Rezazadeh:
  On an Extensible Rule-Based Prover for Event-B. 407
  
• Jacques Julliand, Nicolas Stouls, Pierre-Christophe Bué, Pierre-Alain Masson:
  B Model Abstraction Combining Syntactic and Semantic Methods. 408
  
• Jennifer Sorge, Michael Poppleton, Michael Butler:
  A Basis for Feature-Oriented Modelling in Event-B. 409
  
• Pascal André, Gilles Ardourel, Christian Attiogbé, Arnaud Lanoix:
  Using Event-B to Verify the Kmelia Components and Their Assemblies. 410
  
• Thiago C. de Sousa, Aryldo G. Russo:
  Starting B Specifications from Use Cases. 411
  
• Alessandro Cavalcante Gurgel, Valério Gutemberg de Medeiros, Marcel Vinicius Medeiros Oliveira, David Boris Paul Déharbe:
  Integrating SMT-Solvers in Z and B Tools. 412-413
  
• James R. Williams, Fiona A. C. Polack, Richard F. Paige:
  Formal Analysis in Model Management: Exploiting the Power of CZT. 414
  

Last update Sun May 19 21:36:57 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page