Tools and Algorithms for the Construction and Analysis of Systems

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