Tools and Algorithms for the Construction and Analysis of Systems 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings

Robots at the Edge of the Cloud.- FindingRecurrent Sets with Backward Analysis and Trace Partitioning.- Tactics for theDafny Program Verifier.- Synthesizing Ranking Functions from Bits and Pieces.- AbstractionRefinement and Antichains for Trace Inclusion of Infinite State Systems.- Probabilisticand Stochastic Systems Efficient Syntax-driven Lumping of DifferentialEquations.- Faster Statistical Model Checking for Unbounded TemporalProperties.- Safety-constrained Reinforcement Learning for MDPs.- Safety Verificationof Continuous-Space Pure Jump Markov Processes.- Abstract Learning Frameworksfor Synthesis.- Synthesizing Piece-wise Functions by Learning Classifiers.- AnAutomaton Learning Approach to Solving Safety Games over Infinite Graphs.-Uncertainty Propagation using Probabilistic Affine Forms and Concentration ofMeasure Inequalities.- Online and Compositional Learning of Controllers withApplication to Floor Heating.- Deductive Proofs of Almost Sure Persistence andRecurrence Properties.- Probabilistic CTL* : The Deductive Way.- ParametricRuntime Verification of C Programs.- Coqoon: an IDE for interactive proofdevelopment in Coq.- Multi-core symbolic bisimulation minimization.- Advancesin Symbolic Probabilistic Model Checking with PRISM.- PRISM-PSY: PreciseGPU-Accelerated Parameter Synthesis for Stochastic Systems.- T2: Temporal PropertyVerification.- RTD-Finder: A Tool for Compositional Verification of Real-Time Component-basedSystems.- TcT: Tyrolean Complexity Tool.- Integrated Environment for DiagnosingVerification Errors.- JDart: A Dynamic Symbolic Analysis Framework.- DiagnosticInformation for Control-Flow Analysis of Workflow Graphs.- Approaching theCoverability Problem Continuously.- On Atomicity in Presence of Non-atomicWrites.- Formalizing and Checking Thread Refinement for Data-Race-Free ExecutionModels.- The xSAP Safety Analysis Platform.- FACT: A Probabilistic ModelChecker for Formal Verification with Confidence Intervals.- PrDK: ProtocolProgramming with Automata.- DLC: Compiling a Concurrent System Formal Specificationto a Distributed Implementation.- PRISM-games 2.0: A Tool for Multi-ObjectiveStrategy Synthesis for Stochastic Games.- Cerberus: Automated Synthesis ofEnforcement Mechanisms for Security-sensitive Business Processes.- Developing& Debugging Proof Strategies by Tinkering.- v2c - A Verilog to C TranslatorTool.- Parameterized Compositional Model Checking.- An O(m log n) Algorithm forStuttering Equivalence and Branching Bisimulation.- Interpolants in NonlinearTheories over the Reals.- PTIME Computation of Transitive Closures of OctagonalRelations.- Verification of Linear Controller Software.- Partial OrderReduction for Event-driven Multi-threaded Programs.- Acceleration in Multi-PushdownSystems.- Reduction of Nondeterministic Tree Automata.- Online Timed PatternMatching using Derivatives.- Hybridization based CEGAR for Hybrid Automata withAffine Dynamics.- Complementing Semi-deterministic Buechi Automata.- ReasoningAbout Information Flow Security of Separation Kernels with Channel-basedCommunication.- Some Complexity Results for Stateful Network Verification.- CharacteristicFormulae for Session Types.- Bit-Vector Optimization.- Runtime Monitoring withUnion-Find Structures.- Competition on Software Verification: SV-COMP.- Reliable and Reproducible Competition Results withBenchExec and Witnesses (Report on SV-COMP 2016).