Robots at the Edge of the Cloud -- Finding Recurrent Sets with Backward Analysis and Trace Partitioning -- Tactics for the Dafny Program Verifier -- Synthesizing Ranking Functions from Bits and Pieces -- Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems -- Probabilistic and Stochastic Systems Efficient Syntax-driven Lumping of Differential Equations -- Faster Statistical Model Checking for Unbounded Temporal Properties -- Safety-constrained Reinforcement Learning for MDPs -- Safety Verification of Continuous-Space Pure Jump Markov Processes -- Abstract Learning Frameworks for Synthesis -- Synthesizing Piece-wise Functions by Learning Classifiers -- An Automaton Learning Approach to Solving Safety Games over Infinite Graphs -- Uncertainty Propagation using Probabilistic Affine Forms and Concentration of Measure Inequalities -- Online and Compositional Learning of Controllers with Application to Floor Heating -- Deductive Proofs of Almost Sure Persistence and Recurrence Properties -- Probabilistic CTL* : The Deductive Way -- Parametric Runtime Verification of C Programs -- Coqoon: an IDE for interactive proof development in Coq -- Multi-core symbolic bisimulation minimization -- Advances in Symbolic Probabilistic Model Checking with PRISM -- PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems -- T2: Temporal Property Verification -- RTD-Finder: A Tool for Compositional Verification of Real-Time Component-based Systems -- TcT: Tyrolean Complexity Tool -- Integrated Environment for Diagnosing Verification Errors -- JDart: A Dynamic Symbolic Analysis Framework -- Diagnostic Information for Control-Flow Analysis of Workflow Graphs -- Approaching the Coverability Problem Continuously -- On Atomicity in Presence of Non-atomic Writes -- Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models -- The xSAP Safety Analysis Platform -- FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals -- PrDK: Protocol Programming with Automata -- DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation -- PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games -- Cerberus: Automated Synthesis of Enforcement Mechanisms for Security-sensitive Business Processes -- Developing & Debugging Proof Strategies by Tinkering -- v2c - A Verilog to C Translator Tool -- Parameterized Compositional Model Checking -- An O(m log n) Algorithm for Stuttering Equivalence and Branching Bisimulation -- Interpolants in Nonlinear Theories over the Reals -- PTIME Computation of Transitive Closures of Octagonal Relations -- Verification of Linear Controller Software -- Partial Order Reduction for Event-driven Multi-threaded Programs -- Acceleration in Multi-Pushdown Systems -- Reduction of Nondeterministic Tree Automata -- Online Timed Pattern Matching using Derivatives -- Hybridization based CEGAR for Hybrid Automata with Affine Dynamics -- Complementing Semi-deterministic Buechi Automata -- Reasoning About Information Flow Security of Separation Kernels with Channel-based Communication -- Some Complexity Results for Stateful Network Verification -- Characteristic Formulae for Session Types -- Bit-Vector Optimization -- Runtime Monitoring with Union-Find Structures -- Competition on Software Verification: SV-COMP -- Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP 2016).