Verification, Model Checking, and Abstract Interpretation

A Model-Constructing Satisfiability Calculus.- Automata as Proofs.- Complete Abstractions Everywhere.- Abstraction-Guided Synthesis.- SMT-Based Bisimulation Minimisation of Markov Models.- Hybrid Automata-Based CEGAR for Rectangular Hybrid Systems.- Quantifying Information Leakage of Randomized Protocols.- Reductions for Synthesis Procedures.- Towards Efficient Parameterized Synthesis.- Automatic Inference of Necessary Preconditions.- Fixpoint Computation in the Polyhedra Abstract Domain Using Convex and Numerical Analysis Tools.- SMT-Based Array Invariant Generation.- Flow-Sensitive Fault Localization.- Static Analysis of String Encoders and Decoders.- Robustness Analysis of Networked Systems.- Causality Checking for Complex System Models.- ClabureDB: Classified Bug-Reports Database: Tool for Developers of Program Analysis Tools.- Tool Integration with the Evidential Tool Bus.- Compositional and Lightweight Dependent Type Inference for ML.- Abstract Read Permissions: Fractional Permissions without the Fractions.- Sound and Complete Flow Typing with Unions, Intersections and Negations.- Knockout Prediction for Reaction Networks with Partial Kinetic Information.- Reduced Product Combination of Abstract Domains for Shapes.- Abstraction of Syntax.- Logico-Numerical Max-Strategy Iteration.- A Constraint Solver Based on Abstract Domains.- An Abstract Interpretation of DPLL(T).- All for the Price of Few: (Parameterized Verification through View Abstraction).- Uncovering Symmetries in Irregular Process Networks.- State Space Reduction for Sensor Networks Using Two-Level Partial Order Reduction.- Compositional Sequentialization of Periodic Programs.