Formal Methods and Software Engineering

Invited Papers.- Seamless Model Driven Systems Engineering Based on Formal Models.- Compositional Verification of Input-Output Conformance via CSP Refinement Checking.- Testing I.- Symbolic Query Exploration.- Event Listener Analysis and Symbolic Execution for Testing GUI Applications.- An Empirical Study of Structural Constraint Solving Techniques.- Protocols.- Improving Automatic Verification of Security Protocols with XOR.- Modeling and Verification of Privacy Enhancing Protocols.- Role-Based Symmetry Reduction of Fault-Tolerant Distributed Protocols with Language Support.- Testing II.- Implementing and Applying the Stocks-Carrington Framework for Model-Based Testing.- A Statistical Approach to Test Stochastic and Probabilistic Systems.- Qualitative Action Systems.- Verification.- RAFFS: Model Checking a Robust Abstract Flash File Store.- European Train Control System: A Case Study in Formal Verification.- Development of Security Software: A High Assurance Methodology.- Model Checking I.- Bounded Semantics of CTL and SAT-Based Verification.- Graded-CTL: Satisfiability and Symbolic Model Checking.- Approximate Model Checking of PCTL Involving Unbounded Path Properties.- Object-Orientation.- A Graph-Based Operational Semantics of OO Programs.- Modeling and Analysis of Thread-Pools in an Industrial Communication Platform.- A Verification System for Distributed Objects with Asynchronous Method Calls.- Model checking II.- A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties.- Scalable Multi-core Model Checking Fairness Enhanced Systems.- Combining Static Model Checking with Dynamic Enforcement Using the Statecall Policy Language.- Event-B.- Supporting Reuse of Event-B Developments through Generic Instantiation.- A Lazy Unbounded Model Checker for Event-B.- Proof Assisted Model Checking for B.- Compilation.- Machine-Checked Sequencer for Critical Embedded Code Generator.- Implementing a Direct Method for Certificate Translation.-