Variations on Safety -- Decision Procedures and their Application in Analysis Decision Procedures for Flat Array Properties -- SATMC: A SAT-Based Model Checker for Security-Critical Systems -- IC3 Modulo Theories via Implicit Predicate Abstraction -- SMT-Based Verification of Software Countermeasures against Side-Channel Attacks -- Detecting Unrealizable Specifications of Distributed Systems -- Synthesizing Safe Bit-Precise Invariants -- PEALT: An Automated Reasoning Tool for Numerical Aggregation of Trust Evidence -- GRASShopper: Complete Heap Verification with Mixed Specifications -- Alternating Runtime and Size Complexity Analysis of Integer Programs -- Proving Non termination via Safety -- Ranking Templates for Linear Loops -- Modeling and Model Checking Discrete Systems FDR3 — A Modern Refinement Checker for CSP -- Concurrent Depth-First Search Algorithms -- Basic Problems in Multi-View Modeling -- GPU explore: Many-Core On-the-Fly State Space Exploration Using GPUs -- Forward Reachability Computation for Autonomous Max-Plus-Linear Systems -- Compositional Invariant Generation for Timed Systems -- Characterizing Algebraic Invariants by Differential Radical Invariants -- Quasi-Equal Clock Reduction: More Networks, More Queries -- Are Timed Automata Bad for a Specification Language? Language Inclusion Checking for Timed Automata -- Monitoring, Fault Detection and Identification Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic -- Monitoring Modulo Theories -- Temporal-Logic Based Runtime Observer Pairs for System Health Management of Real-Time Systems -- Status Report on Software Verification (Competition Summary SV-COMP 2014) -- CBMC – C Bounded Model Checker (Competition Contribution) -- CPAchecker with Sequential Combination of Explicit-Value Analyses and Predicate Analyses (Competition Contribution) -- CPALIEN: Shape Analyzer for CPAChecker (Competition Contribution) -- Lazy-CSeq: A Lazy Sequentialization Tool for C (Competition Contribution) -- MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings (Competition Contribution) -- ESBMC 1.22 (Competition Contribution) -- FrankenBit: Bit-Precise Verification with Many Bits (Competition Contribution) -- Predator: A Shape Analyzer Based on Symbolic Memory Graphs (Competition Contribution) -- Symbiotic 2: More Precise Slicing (Competition Contribution) -- Ultimate Automizer with Unsatisfiable Cores (Competition Contribution) -- Ultimate Kojak (Competition Contribution) -- Specifying and Checking Linear Time Properties Discounting in LTL -- Symbolic Model Checking of Stutter-Invariant Properties Using Generalized Testing Automata -- Symbolic Synthesis for Epistemic Specifications with Observational Semantics -- Synthesis for Human-in-the-Loop Control Systems -- Learning Regular Languages over Large Alphabets -- Verification of Concurrent Quantum Protocols by Equivalence Checking -- Computing Conditional Probabilities in Markovian Models Efficiently -- Permissive Controller Synthesis for Probabilistic Systems -- Precise Approximations of the Probability Distribution of a Markov Process in Time: An Application to Probabilistic Invariance -- SACO: Static Analyzer for Concurrent Objects -- VeriMAP: A Tool for Verifying Programs through Transformations -- CIF 3: Model-Based Engineering of Supervisory Controllers -- EDD: A Declarative Debugger for Sequential Erlang Programs -- APTE: An Algorithm for Proving Trace Equivalence -- The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification -- Bounds2: A Tool for Compositional Multi-parametrised Verification -- On the Correctness of a Branch Displacement Algorithm -- Analyzing the Next Generation Airborne Collision Avoidance System -- Environment-Model Based Testing of Control Systems: Case Studies.