Integrated Formal Methods

Invited Contributions.- Can Formal Methods Improve the Efficiency of Code Reviews.-Symbolic Computation and Automated Reasoning for Program Analysis.- Program verification.- On Type Checking Delta-Oriented Product Lines.- Verifying a priority scheduler for an SCJ runtime environment.- Why Just Boogie? Translating Between Intermediate Verification Languages.- Probabilistic systems.- Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata.- Probabilistic Formal Analysis of App Usage to Inform Redesign.- Extension of PRISM by Synthesis of Optimal Timeouts in Fixed-Delay CTMC.- Concurrency.- Monitoring Multi-threaded Component-Based Systems.- A Generalised Theory of Interface Automata, Component Compatibility and Error.- On Implementing a Monitor-Oriented Programming Framework for Actor Systems.- Towards a Thread-Local Proof Technique for Starvation Freedom.- Reasoning about Inheritance and Unrestricted Reuse in Object-Oriented Concurrent Systems.- A Formal Model of the Safety-Critical Java Level 2 Paradigm.- Safety and liveness.- Deciding Monadic Second Order Logic over omega-words by Specialized Finite Automata.- Property Preservation for Extension Patterns of State Transition Diagrams.- Symbolic Reachability Analysis of B through ProB and LTSmin.- Model learning.- Enhancing Automata Learning by Log-Based Metrics.- Refactoring of Legacy Software using Model Learning and Equivalence Checking: an Industrial Experience Report.- On Robust Malware Classifiers by Verifying Unwanted Behaviours.- SAT and SMT solving.- Efficient Deadlock-Freedom Checking using Local Analysis and SAT Solving.- SMT Solvers for Validation of B and Event-B models.- Avoiding Medication Conflicts for Patients with Multimorbidities.- Testing.- Temporal Random Testing for Spark Streaming.- Combining Static Analysis and Testing for Deadlock Detection.- Fuzzing JavaScript Engine APIs.- Theorem proving and constraint satisfaction.- A Component-based Approach to Hybrid Systems Safety Verification.- Verifying Pointer Programs using Separation Logic and Invariant Based Programming in Isabelle.- A Constraint Satisfaction Method for Configuring Non-Local Service Interfaces.- Case studies.- Rule-based Consistency Checking of Railway Infrastructure Designs.- Formal Verification of Safety PLC Based Control Software.- Enabling Static Driver Verifier using Microsoft Azure.