Automated Technology for Verification and Analysis

Keynote Speeches.- Analysis of Recursive Probabilistic Models.- Verification Challenges and Opportunities in the New Era of Microprocessor Design.- Automated Abstraction of Software.- Regular Papers.- Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives.- Eager Markov Chains.- A Probabilistic Learning Approach for Counterexample Guided Abstraction Refinement.- A Fine-Grained Fullness-Guided Chaining Heuristic for Symbolic Reachability Analysis.- Model Checking Timed Systems with Urgencies.- Whodunit? Causal Analysis for Counterexamples.- On the Membership Problem for Visibly Pushdown Languages.- On the Construction of Fine Automata for Safety Properties.- On the Succinctness of Nondeterminism.- Efficient Algorithms for Alternating Pushdown Systems with an Application to the Computation of Certificate Chains.- Compositional Reasoning for Hardware/Software Co-verification.- Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition.- On the Satisfiability of Modular Arithmetic Formulae.- Selective Approaches for Solving Weak Games.- Controller Synthesis and Ordinal Automata.- Effective Contraction of Timed STGs for Decomposition Based Timed Circuit Synthesis.- Synthesis for Probabilistic Environments.- Branching-Time Property Preservation Between Real-Time Systems.- Automatic Verification of Hybrid Systems with Large Discrete State Space.- Timed Unfoldings for Networks of Timed Automata.- Symbolic Unfoldings for Networks of Timed Automata.- Ranked Predicate Abstraction for Branching Time: Complete, Incremental, and Precise.- Timed Temporal Logics for Abstracting Transient States.- Predicate Abstraction of Programs with Non-linear Computation.- A Fresh Look at Testing for Asynchronous Communication.- Proactive Leader Election in Asynchronous Shared Memory Systems.- A Semantic Framework for Test Coverage.- Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols.- Analyzing Security Protocols in Hierarchical Networks.- Functional Analysis of a Real-Time Protocol for Networked Control Systems.- Symbolic Semantics for the Verification of Security Properties of Mobile Petri Nets.- Sigref - A Symbolic Bisimulation Tool Box.- Towards a Model-Checker for Counter Systems.- The Implementation of Mazurkiewicz Traces in POEM.- Model-Based Tool-Chain Infrastructure for Automated Analysis of Embedded Systems.