Automated Technology for Verification and Analysis, 2014 12th International Symposium, ATVA 2014, Sydney, Australia, November 3-7, 2014, Proceedings Programming and Software Engineering Series

Verifying Communicating Multi-pushdown Systems via Split-Width.- Booster: An Acceleration-Based Verification Framework for Array Programs.- A Bounded Model Checker for SPARK Programs.- Acceleration of Affine Hybrid Transformations.- A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol.- Quantitative Verification of Weighted Kripke Structures.- Formal Safety Assessment via Contract-Based Design.- Verification of Markov Decision Processes Using Learning Algorithms.- Test Coverage Estimation Using Threshold Accepting.- On Time with Minimal Expected Cost!.- Fast Debugging of PRISM Models.- ACME: Automata with Counters, Monoids and Equivalence (Tool Paper).-Modelling and Analysis of Markov Reward Automata.- Extensional Crisis and Proving Identity.- Deciding Entailments in Inductive Separation Logic with Tree Automata.- Liveness Analysis for Parameterised Boolean Equation Systems.- Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata.- PeCAn: Compositional Verification of Petri Nets Made Easy.- The Context-Freeness Problem Is coNP-Complete for Flat Counter Systems.- Efficiently and Completely Verifying Synchronized Consistency Models.- Symmetry Reduction in Infinite Games with Finite Branching.- Incremental Encoding and Solving of Cardinality Constraints.- Formal Verification of Skiplists with Arbitrary Many Levels.- Using Flow Specifications of Parameterized Cache Coherence Protocols for Verifying Deadlock Freedom.- A Game-Theoretic Approach to Simulation of Data-Parameterized Systems.- Nested Reachability Approximation for Discrete-Time Markov Chains with Univariate Parameters.- Symbolic Memory with Pointers.- Trace Abstraction Refinement for Timed Automata.- Statistically Sound Verification and Optimization for Complex Systems.