Marcel Vinícius Medeiros Oliveira & James Woodcock 
Formal Methods: Foundations and Applications [PDF ebook] 
12th Brazilian Symposium on Formal Methods, SBMF 2009 Gramado, Brazil, August 19-21, 2009 Revised Selected Papers

Speeding Up Simulation of System C Using Model Checking.- Partial Behaviour Modelling: Foundations for Incremental and Iterative Model-Based Software Engineering.- Satisfiability Modulo Theories: An Appetizer.- Interruption Testing of Reactive Systems.- Test Case Generation of Embedded Real-Time Systems with Interruptions for Free RTOS.- Concurrent Models of Flash Memory Device Behaviour.- Corecursive Algebras: A Study of General Structured Corecursion.- Formalizing Free RTOS: First Steps.- A Mechanized Strategy for Safe Abstraction of CSP Specifications.- Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B.- An Integrated Formal Methods Tool-Chain and Its Application to Verifying a File System Model.- Towards Safe Design of Synchronous Bus Protocols in Event-B.- Mechanising Data-Types for Kernel Design in Z.- A Complete Set of Object Modeling Laws for Alloy.- Undecidability Results for Distributed Probabilistic Systems.- Formalisation and Analysis of Objects as CSP Processes.- Concolic Testing of the Multi-sector Read Operation for Flash Memory File System.- Low-Level Code Verification Based on CSP Models.- Formal Modelling of a Microcontroller Instruction Set in B.- Defining Behaviours by Quasi-finality.- Verifying Compiled File System Code.- Reasoning about General Quantum Programs over Mixed States.- A Simple and General Theoretical Account for Abstract Types.