Automated Technology for Verification and Analysis

Invited Talks.- Tests, Proofs and Refinements.- Formal Verification and Biology.- Trust and Automation in Verification Tools.- Model Checking.- CTL Model-Checking with Graded Quantifiers.- Genetic Programming and Model Checking: Synthesizing New Mutual Exclusion Algorithms.- Computation Tree Regular Logic for Genetic Regulatory Networks.- Compositional Verification for Component-Based Systems and Application.- A Direct Algorithm for Multi-valued Bounded Model Checking.- Software Verification.- Model Checking Recursive Programs with Exact Predicate Abstraction.- Loop Summarization Using Abstract Transformers.- Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions.- Decision Procedures.- Automating Algebraic Specifications of Non-freely Generated Data Types.- Interpolants for Linear Arithmetic in SMT.- SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems.- SMELS: Satisfiability Modulo Equality with Lazy Superposition.- Linear-Time Analysis.- Controllable Test Cases for the Distributed Test Architecture.- Tool Demonstration Papers.- Goanna: Syntactic Software Model Checking.- A Dynamic Assertion-Based Verification Platform for Validation of UML Designs.- CheckSpec: A Tool for Consistency and Coverage Analysis of Assertion Specifications.- DiVinE Multi-Core - A Parallel LTL Model-Checker.- Alaska.- NetQi: A Model Checker for Anticipation Game.- Component-Based Design and Analysis of Embedded Systems with UPPAAL PORT.- Timed and Stochastic Systems.- Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions.- Decidable Compositions of O-Minimal Automata.- On the Applicability of Stochastic Petri Nets for Analysis of Multiserver Retrial Systems with Different Vacation Policies.- Model Based Importance Analysis for Minimal Cut Sets.- Theory.- Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic.- Tree Pattern Rewriting Systems.- Deciding Bisimilarity of Full BPA Processes