Formal methods [electronic resource] : foundations and applications : 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009 : revised selected papers / Marcel Vinícius Medeiros Oliveira, Jim Woodcock (eds.)
This book constitutes the thoroughly refereed post-conference proceedings of the 12th Brazilian Symposium on Formal Methods, SBMF 2009, held in Gramado, Brazil, in August 2009 -- co-located with SAST 2009, the Brazilian Workshop on Systematic and Automated Software Testing. The 20 revised full paper...
Saved in:
| Online Access: |
Full Text (via Springer) |
|---|---|
| Corporate Author: | |
| Other Authors: | , |
| Other title: | SBMF 2009. |
| Format: | Electronic Conference Proceeding eBook |
| Language: | English |
| Published: |
Berlin ; New York :
Springer,
©2009.
|
| Series: | Lecture notes in computer science ;
5902. LNCS sublibrary. Programming and software engineering. |
| Subjects: |
Table of Contents:
- 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.