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
SystemsSafety 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.
