default search action
ABZ 2010: Orford, QC, Canada
- Marc Frappier, Uwe Glässer, Sarfraz Khurshid, Régine Laleau, Steve Reeves:
Abstract State Machines, Alloy, B and Z, Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings. Lecture Notes in Computer Science 5977, Springer 2010, ISBN 978-3-642-11810-4
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
AsmetaSMV: A Way to Link High-Level ASM Models to Low-Level NuSMV Specifications. 61-74 - Elvinia Riccobene
An Executable Semantics of the SystemC UML Profile. 75-90
Alloy Papers
- Alban Tiberghien, Philippe Merle
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 S. Khoury, Chaouki T. Abdallah
Towards Formalizing Network Architectural Descriptions. 132-145 - Mark C. Reynolds:
Lightweight Modeling of Java Virtual Machine Security Constraints. 146-159 - Nicolás D'Ippolito
Alloy+HotCore: A Fast Approximation to Unsat Core. 160-173
B Papers
- Alexei Iliasov, Elena Troubitsyna, Linas Laibinis, Alexander B. Romanovsky
Supporting Reuse in Event B Development: Modularisation Approach. 174-188 - Andrew Ireland, Gudmund Grov, Michael J. 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
A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking. 231-244 - Mamoun Filali-Amine, Julia Lawall:
Development of a Synchronous Subset of AADL. 245-258 - Néstor Cataño
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
Communication Systems in ClawZ. 334-348 - Mark Slaymaker
Formalising and Validating RBAC-to-XACML Translation Using Lightweight Formal Methods. 349-362 - Nicolas Wu
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
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
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
Code Synthesis for Timed Automata: A Comparison Using Case Study. 403 - Atif Mashkoor
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 J. Butler, Andrew Edmunds, Abdolbaghi Rezazadeh:
On an Extensible Rule-Based Prover for Event-B. 407 - Jacques Julliand, Nicolas Stouls
B Model Abstraction Combining Syntactic and Semantic Methods. 408 - Jennifer Sorge, Michael Poppleton, Michael J. Butler
A Basis for Feature-Oriented Modelling in Event-B. 409 - Pascal André, Gilles Ardourel, J. Christian Attiogbé
Using Event-B to Verify the Kmelia Components and Their Assemblies. 410 - Thiago C. de Sousa
Starting B Specifications from Use Cases. 411 - Alessandro Cavalcante Gurgel, Valério Gutemberg de Medeiros, Marcel Vinícius 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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-12-19 22:18 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: