Formal Methods: Foundations and Applications

Speeding Up Simulation of SystemC 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 FreeRTOS.- Concurrent Models of Flash Memory Device Behaviour.- Corecursive Algebras: A Study of General Structured Corecursion.- Formalizing FreeRTOS: 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.