Computer Aided Verification

Automata Networks.- Model-Checking Signal Transduction Networks through Decreasing Reachability Sets.- TTP: Tool for Tumor Progression.- Exploring Parameter Space of Stochastic Biochemical Systems using Quantitative Model Checking.- Parameterized Verification of Asynchronous Shared-Memory Systems.- Partial Orders for Efficient BMC of Concurrent Software.- Incremental, Inductive Coverability.- Automatic linearizability proofs of concurrent objects with cooperating.- Updates.- Duet: Static Analysis for Unbounded Parallelism.- SVA and PSL Local Variables.- A Practical Approach.- Formal Verification of Hardware Synthesis.- CacBDD: A BDD Package with Dynamic Cache Management.- Distributed Explicit State Model Checking of Deadlock Freedom.- Exponential-Condition-Based Barrier Certificate Generation for Safety.- Verification of Hybrid Systems .- Efficient Robust Monitoring for STL.- Abstraction based Model-Checking of Stability of Hybrid Systems.- Faster Algorithms for Markov Decision Processes with Low Tree width.- Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis.- Importance Splitting for Statistical Model Checking Rare Properties.- Minimal Sets over Monotone Predicates in Boolean Formulae.- Smten: Automatic Translation of High-level Symbolic Computations into SMT Queries.- QUAIL: a quantitative security analyzer for imperative code.- Effectively Propositional Reasoning about Reachability in Linked Data Structures.- Learning Universally Quantified Invariants of Linear Data Structures.- GOAL for Games, Omega-Automata, and Logics.- Efficient synthesis for concurrency using semantics-preserving Transformations.