Computer Aided Verification

Invited Tutorials.- Transactional Memory: Glimmer of a Theory.- Mixed-Signal System Verification: A High-Speed Link Example.- Modelling Epigenetic Information Maintenance: A Kappa Tutorial.- Component-Based Construction of Real-Time Systems in BIP.- Invited Talks.- Models and Proofs of Protocol Security: A Progress Report.- Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after?.- SPEED: Symbolic Complexity Bound Analysis.- Regression Verification: Proving the Equivalence of Similar Programs.- Regular Papers.- Symbolic Counter Abstraction for Concurrent Software.- Priority Scheduling of Distributed Systems Based on Model Checking.- Explaining Counterexamples Using Causality.- Size-Change Termination, Monotonicity Constraints and Ranking Functions.- Linear Functional Fixed-points.- Better Quality in Synthesis through Quantitative Objectives.- Automatic Verification of Integer Array Programs.- Automated Analysis of Java Methods for Confidentiality.- Requirements Validation for Hybrid Systems.- Towards Performance Prediction of Compositional Models in Industrial GALS Designs.- Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion.- Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers.- Meta-analysis for Atomicity Violations under Nested Locking.- An Antichain Algorithm for LTL Realizability.- On Extending Bounded Proofs to Inductive Proofs.- Games through Nested Fixpoints.- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories.- Software Transactional Memory on Relaxed Memory Models.- Sliding Window Abstraction for Infinite Markov Chains.- Centaur Technology Media Unit Verification.- Incremental Instance Generation in Local Reasoning.- Quantifier Elimination via Functional Composition.- Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique.- Replacing Testing with Formal Verification in Intel CoreTMi7