---

This book
constitutes the refereed proceedings of the 12th International Conference on Integrated
Formal Methods, IFM 2016, held in Reykjavik, Iceland, in June 2016.
The 33 papers
presented in this volume were carefully reviewed and selected from 99
submissions. They were organized in topical sections named: invited
contributions; program verification; probabilistic systems; concurrency; safetyand liveness; model learning; SAT and SMT solving; testing; theorem proving and
constraint satisfaction; case studies.

---

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 Hybrid04
ystems 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.

---