Automated Technology for Verification and Analysis: 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014, Proceedings

Front Matter....Pages -
Verifying Communicating Multi-pushdown Systems via Split-Width....Pages 1-17
Booster: An Acceleration-Based Verification Framework for Array Programs....Pages 18-23
A Bounded Model Checker for SPARK Programs....Pages 24-30
Acceleration of Affine Hybrid Transformations....Pages 31-46
A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol....Pages 47-63
Quantitative Verification of Weighted Kripke Structures....Pages 64-80
Formal Safety Assessment via Contract-Based Design....Pages 81-97
Verification of Markov Decision Processes Using Learning Algorithms....Pages 98-114
Test Coverage Estimation Using Threshold Accepting....Pages 115-128
On Time with Minimal Expected Cost!....Pages 129-145
Fast Debugging of PRISM Models....Pages 146-162
ACME: Automata with Counters, Monoids and Equivalence....Pages 163-167
Modelling and Analysis of Markov Reward Automata....Pages 168-184
Extensional Crisis and Proving Identity....Pages 185-200
Deciding Entailments in Inductive Separation Logic with Tree Automata....Pages 201-218
Liveness Analysis for Parameterised Boolean Equation Systems....Pages 219-234
Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata....Pages 235-241
PeCAn: Compositional Verification of Petri Nets Made Easy....Pages 242-247
The Context-Freeness Problem Is coNP-Complete for Flat Counter Systems....Pages 248-263
Efficiently and Completely Verifying Synchronized Consistency Models....Pages 264-280
Symmetry Reduction in Infinite Games with Finite Branching....Pages 281-296
Incremental Encoding and Solving of Cardinality Constraints....Pages 297-313
Formal Verification of Skiplists with Arbitrary Many Levels....Pages 314-329
Using Flow Specifications of Parameterized Cache Coherence Protocols for Verifying Deadlock Freedom....Pages 330-347
A Game-Theoretic Approach to Simulation of Data-Parameterized Systems....Pages 348-363
Nested Reachability Approximation for Discrete-Time Markov Chains with Univariate Parameters....Pages 364-379
Symbolic Memory with Pointers....Pages 380-395
Trace Abstraction Refinement for Timed Automata....Pages 396-410
Statistically Sound Verification and Optimization for Complex Systems....Pages 411-427
Back Matter....Pages -