John Derrick, John A. Fitzgerald, Stefania Gnesi, Sarfraz Khurshid, Michael Leuschel, Steve Reeves, Elvinia Riccobene (Eds.): Abstract State Machines, Alloy, B, VDM, and Z - Third International Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings. Springer 2012 Lecture Notes in Computer Science ISBN 978-3-642-30884-0
Invited Talks
Egon Börger, Antonio Cisternino, Vincenzo Gervasi: Contribution to a Rigorous Analysis of Web Application Frameworks. 1-20
Ian J. Hayes, Robert Colvin: Integrated Operational Semantics: Small-Step, Big-Step and Multi-step. 21-35
ASM Papers
Paolo Arcaini, Francesco Bolis, Angelo Gargantini: Test Generation for Sequential Nets of Abstract State Machines. 36-50
Richard Banach, Huibiao Zhu, Wen Su, Xiaofeng Wu: Continuous ASM, and a Pacemaker Sensing Fragment. 65-78
Vincenzo Gervasi: An ASM Model of Concurrency in a Web Browser. 79-93
Alloy Papers
Benoît Fraikin, Marc Frappier, Richard St.-Denis: Modeling the Supervisory Control Theory with Alloy. 94-107

Timothy Nelson, Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi: Toward a More Complete Alloy. 136-149

B Papers


Gudmund Grov, Andrew Ireland, Maria Teresa Llano: Refinement Plans for Informed Formal Design. 208-222
David Mentré, Claude Marché, Jean-Christophe Filliâtre, Masashi Asuka: Discharging Proof Obligations from Atelier B Using Multiple Automated Provers. 238-251
VDM Papers
Cliff B. Jones, Matthew J. Lovert, L. Jason Steggles: A Semantic Analysis of Logics That Cope with Partial Terms. 252-265
Claus Ballegaard Nielsen, Kenneth Lausdahl, Peter Gorm Larsen: Combining VDM with Executable Code. 266-279
Z Papers
Maximiliano Cristiá, Claudia S. Frydman: Extending the Test Template Framework to Deal with Axiomatic Descriptions, Quantifiers and Set Comprehensions. 280-293
Chris Marriott, Frank Zeyda, Ana Cavalcanti: A Tool Chain for the Automatic Generation of Circus Specifications of Simulink Diagrams. 294-307
Ramsay Taylor: Verification of Hardware Interaction Properties of Software. 308-322
ASM Short Papers
Matthes Elstermann, Detlef Seese, Albert Fleischmann: Using the Arbitrator Pattern for Dynamic Process-Instance Extension in a Work-Flow Management System. 323-326
Roland Lezuo, Andreas Krall: A Unified Processor Model for Compiler Verification and Simulation Using ASM. 327-330
Andrea Luzzana, Mattia Rossetti, Paolo Righettini, Patrizia Scandurra: Modeling Synchronization/Communication Patterns in Vision-Based Robot Control Applications Using ASMs. 331-335
Raffaela Mirandola, Pasqualina Potena, Patrizia Scandurra: A Reliability Prediction Method for Abstract State Machines. 336-340
Hamed Yaghoubi Shahir, Roozbeh Farahbod, Uwe Glässer: Refactoring Abstract State Machine Models. 345-348
B Short Papers
Richard Banach, Huibiao Zhu, Wen Su, Xiaofeng Wu: Continuous Behaviour in Event-B: A Sketch. 349-352
Thiago C. de Sousa, Paulo Sérgio Muniz Silva, Colin F. Snook: A Practical Event-B Refinement Method Based on a UML-Driven Development Process. 357-360
Ionut Dinca, Florentin Ipate, Laurentiu Mierla, Alin Stefanescu: Learn and Test for Event-B - A Rodin Plugin. 361-364
Andrew Edmunds, Michael Butler, Issam Maamria, Renato Silva, Chris Lovell: Event-B Code Generation: Type Extension with Theories. 365-368
Denis Sabatier, Lilian Burdy, Antoine Requet, Jérôme Guéry: Formal Proofs for the NYCT Line 7 (Flushing) Modernization Project. 369-372
Gintautas Sulskus, Michael Poppleton: A Pattern for Modelling Fault Tolerant Systems in Event-B. 373-376



