Keynote Paper.- A Flight Rule Checkerfor the LADEE Lunar Spacecraft.- Regular Papers.- Proof-theoretic Conservative Extension of HOL with Ad-hoc Overloading.- A Myhill-Nerode Theorem for Register Automata and Symbolic Trace Languages.- CiMPG+F: A Proof Generator & Fixer-upper for CafeOBJ Specifications.- Statistical Analysis of Non-Deterministic Fork-Join Processes.- On Two Characterizations of Feature Models.- The Complexity of Boolean State Separation.- Occupancy Number Restricted Boolean Petri Net Synthesis: A Fixed-Parameter Algorithm.- Star-freeness, First-order Definability and Aperiodicity of Structured Context-free Languages.- Formal Verification of Parallel Stream Compaction and Summed-Area Table Algorithms.- Compositionality of Safe Communication in Systems of Team Automata.- Analysis of Bayesian Networks via Prob-Solvable Loops.- Semantics of a Relational Lambda-Calculus.- Implementing Hybrid Semantics: From Functional to Imperative.- Implementation correctness for Replicated Data Types, categorically.- Tool Paper.- Qsimulation V2.0: an Optimized Quantum Simulator.