Tools and Algorithms for the Construction and Analysis of Systems

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