Tools and Algorithms for the Construction and Analysis of Systems

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