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 updated on Fri May 24 04:37:52 2013 by the dblp team
data released under the ODC-BY 1.0 license
see also our legal information page