FM 2016: Formal Methods: 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings

Front Matter....Pages I-XXIII
Front Matter....Pages 1-1
Industrial-Strength Model-Based Testing of Safety-Critical Systems....Pages 3-22
Front Matter....Pages 23-23
Counter-Example Guided Program Verification....Pages 25-42
Tighter Reachability Criteria for Deadlock-Freedom Analysis....Pages 43-59
Compositional Parameter Synthesis....Pages 60-68
Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor....Pages 69-84
A Model Checking Approach to Discrete Bifurcation Analysis....Pages 85-101
State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI....Pages 102-118
Formal Verification of Multi-Paxos for Distributed Consensus....Pages 119-136
Validated Simulation-Based Verification of Delayed Differential Dynamics....Pages 137-154
Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation....Pages 155-163
From Electrical Switched Networks to Hybrid Automata....Pages 164-181
Danger Invariants....Pages 182-198
Local Planning of Multiparty Interactions with Bounded Horizons....Pages 199-216
Finding Suitable Variability Abstractions for Family-Based Analysis....Pages 217-234
Recovering High-Level Conditions from Binary Programs....Pages 235-253
Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations....Pages 254-273
Exploring Model Quality for ACAS X....Pages 274-290
Learning Moore Machines from Input-Output Traces....Pages 291-309
Modal Kleene Algebra Applied to Program Correctness....Pages 310-325
Mechanised Verification Patterns for Dafny....Pages 326-343
Front Matter....Pages 23-23
Formalising and Validating the Interface Description in the FMI Standard....Pages 344-351
An Algebra of Synchronous Atomic Steps....Pages 352-369
Error Invariants for Concurrent Traces....Pages 370-387
An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for the LEON3 Processor....Pages 388-405
Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow....Pages 406-425
A Generic Logic for Proving Linearizability....Pages 426-443
Refactoring Refinement Structure of Event-B Machines....Pages 444-459
Towards Concolic Testing for Hybrid Systems....Pages 460-478
Explaining Relaxed Memory Models with Program Transformations....Pages 479-495
SpecCert: Specifying and Verifying Hardware-Based Security Enforcement....Pages 496-512
Automated Verification of Timed Security Protocols with Clock Drift....Pages 513-530
Dealing with Incompleteness in Automata-Based Model Checking....Pages 531-550
Equivalence Checking of a Floating-Point Unit Against a High-Level C Model....Pages 551-558
Battery-Aware Scheduling in Low Orbit: The GomX–3 Case....Pages 559-576
Discounted Duration Calculus....Pages 577-592
Sound and Complete Mutation-Based Program Repair....Pages 593-611
An Implementation of Deflate in Coq....Pages 612-627
Decoupling Abstractions of Non-linear Ordinary Differential Equations....Pages 628-644
Regression Verification for Unbalanced Recursive Functions....Pages 645-658
Automated Mutual Explicit Induction Proof in Separation Logic....Pages 659-676
Front Matter....Pages 23-23
Finite Model Finding Using the Logic of Equality with Uninterpreted Functions....Pages 677-693
GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking....Pages 694-701
Approximate Bisimulation and Discretization of Hybrid CSP....Pages 702-720
A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems....Pages 721-738
Front Matter....Pages 739-739
Model-Based Design of an Energy-System Embedded Controller Using Taste ....Pages 741-747
Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems....Pages 748-756
Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller....Pages 757-763
Taming Interrupts for Verifying Industrial Multifunction Vehicle Bus Controllers....Pages 764-771
Rule-Based Incremental Verification Tools Applied to Railway Designs and Regulations....Pages 772-778
RIVER: A Binary Analysis Framework Using Symbolic Execution and Reversible x86 Instructions....Pages 779-785
Back Matter....Pages 787-789