Formal methods: Foundations and applications : 15th Brazilian Symposium, SBMF 2012, Natal, Brazil, September 23-28, 2012. Proceedings / Rohit Gheyi, David Naumann (eds.).

The Versatile Synchronous Observer / John Rushby -- Thirteen Years of Automated Code Analysis at Microsoft / Wolfram Schulte -- Model Checking Propositional Deontic Temporal Logic via a [mu]-Calculus Characterization / Araceli Acosta, Cecilia Kilmurray, Pablo F. Castro and Nazareno M. Aguirre -- An Approach Using the B Method to Formal Verification of PLC Programs in an Industrial Setting / Haniel Barbosa and David Déharbe -- Palytoxin Inhibits the Sodium-Potassium Pump -- An Investigation of an Electrophysiological Model Using Probabilistic Model Checking / Fernando A.F. Braz, Jader S. Cruz, Alessandra C. Faria-Campos and Sérgio V.A. Campos -- BETA: A B Based Testing Approach / Ernesto C.B. de Matos and Anamaria Martins Moreira -- A Process Algebra Based Strategy for Generating Test Vectors from SCR Specifications / Gustavo Carvalho, Diogo Falcão, Alexandre Mota and Augusto Sampaio -- Specification Patterns for Properties over Reachable States of Graph Grammars / Simone André da Costa Cavalheiro, Luciana Foss and Leila Ribeiro -- Compositionality and Refinement in Model-Driven Engineering / Jim Davies, Jeremy Gibbons, David Milward and James Welch -- Identifying Hardware Failures Systematically / André Didier and Alexandre Mota -- Investigating Time Properties of Interrupt-Driven Programs / Yanhong Huang, Yongxin Zhao, Jianqi Shi, Huibiao Zhu and Shengchao Qin -- Specifying and Verifying Declarative Fluent Temporal Logic Properties of Workflows / Germán Regis, Nicolás Ricci, Nazareno M. Aguirre and Tom Maibaum -- Composition of Model Transformations: A Categorical Framework / Christoph Schulz, Michael Löwe and Harald König -- Verification Rules for Exception Handling in Eiffel / Emil Sekerinski and Tian Zhang -- A Sound Reduction of Persistent-Sets for Deadlock Detection in MPI Applications / Subodh Sharma, Ganesh Gopalakrishnan and Greg Bronevetsky -- Alternating-Time Temporal Logic in the Calculus of (Co)Inductive Constructions / Dante Zanarini, Carlos Luna and Luis Sierra.

Includes bibliographical references and author index.

This book constitutes the refereed proceedings of the 15th Brazilian Symposium on Formal Methods, SBMF 2012, held in Natal, Brazil, in September 2012; co-located with CBSoft 2012, the Third Brazilian Conference on Software: Theory and Practice. The 14 revised full papers presented together with 2 keynotes were carefully reviewed and selected from 29 submissions. The papers presented cover a broad range of foundational and methodological issues in formal methods for the design and analysis of software and hardware systems as well as applications in various domains.