Automated technology for verification and analysis [electronic resource] : 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014, Proceedings / Franck Cassez, Jean-Francois Raskin (eds.).

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.