Formal Methods for Industrial Critical Systems

Invited Papers.- Attacking Large Industrial Code with Bi-abductive Inference.- On a Uniform Framework for the Definition of Stochastic Process Languages.- Applying a Formal Method in Industry: A 15-Year Trajectory.- What’s in Common between Test, Model Checking, and Decision Procedures?.- Contributed Papers.- Verifying Cryptographic Software Correctness with Respect to Reference Implementations.- Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software.- Dynamic State Space Partitioning for External Memory Model Checking.- Compositional Verification of a Communication Protocol for a Remotely Operated Vehicle.- Modeling Concurrent Systems with Shared Resources.- Platform-Specific Restrictions on Concurrency in Model Checking of Java Programs.- Formal Analysis of Non-determinism in Verilog Cell Library Simulation Models.- Preemption Abstraction.- A Rigorous Methodology for Composing Services.- A Certified Implementation on Top of the Java Virtual Machine.- Selected Posters.- Formal Development for Railway Signaling Using Commercial Tools.- Integrated Formal Approach for Qualified Critical Embedded Code Generator.- Visualising Event-B Models with B-Motion Studio.- Behavioural Analysis of an I2C Linux Driver.- Model-Based Testing of Electronic Passports.- Developing a Decision Support Tool for Dam Management with SPIN.