Full Description
This book
constitutes the proceedings of the 22nd International Conference on Tools and
Algorithms for the Construction and Analysis of Systems, TACAS 2016, which took
place in Eindhoven, The Netherlands, in April 2016, held as Part of the
European Joint Conferences on Theory and Practice of Software, ETAPS 2016.
The 44 full papers presented in this volume were carefully reviewed and selected
from 175 submissions. They were organized in topical sections named: abstraction
and verification; probabilistic and stochastic systems; synthesis; tool papers;
concurrency; tool demos; languages and automata; security; optimization; and
competition on software verification - SV-COMP.
Contents
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).
