Invited Contributions.- Weighted Pushdown Systems and Trust-Management Systems.- Parametrization and Slicing.- Automatic Verification of Parameterized Data Structures.- Parameterized Verification of ?-Calculus Systems.- Easy Parameterized Verification of Biphase Mark and 8N1 Protocols.- Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs.- Symbolic Techniques.- New Metrics for Static Variable Ordering in Decision Diagrams.- Widening ROBDDs with Prime Implicants.- Efficient Guided Symbolic Reachability Using Reachability Expressions.- Satisfiability.- SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in a Separation Logic Solver.- SAT-Based Software Certification.- Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants.- Exploration of the Capabilities of Constraint Programming for Software Verification.- Abstraction.- Counterexample-Guided Abstraction Refinement for the Analysis of Graph Transformation Systems.- Why Waste a Perfectly Good Abstraction?.- Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking.- Approximating Predicate Images for Bit-Vector Logic.- Model Checking Algorithms.- Finitary Winning in ?-Regular Games.- Efficient Model Checking for LTL with Partial Order Snapshots.- A Local Shape Analysis Based on Separation Logic.- Program Verification.- Compositional Model Extraction for Higher-Order Concurrent Programs.- A Region Graph Based Approach to Termination Proofs.- Verifying Concurrent Message-Passing C Programs with Recursive Calls.- Automata-Based Verification of Programs with Tree Updates.- Runtime Diagnostics.- An Experimental Comparison of the Effectiveness of Control Flow Based Testing Approaches onSeeded Faults.- Exploiting Traces in Program Analysis.- Quantitative Techniques.- Model-Checking Markov Chains in the Presence of Uncertainties.- Safety Metric Temporal Logic Is Fully Decidable.- Simulation-Based Graph Similarity.- Tool Demonstrations.- PRISM: A Tool for Automatic Verification of Probabilistic Systems.- DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation.- mcmas: A Model Checker for Multi-agent Systems.- MSCan – A Tool for Analyzing MSC Specifications.- Refinement.- A Practical and Complete Approach to Predicate Refinement.- Counterexample Driven Refinement for Abstract Interpretation.- Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems.