Automated Technology for Verification and Analysis: 10th International Symposium, ATVA 2012, Thiruvananthapuram, India, October 3-6, 2012, Proceedings (Lecture Notes in Computer Science, 7561)

This book constitutes the thoroughly refereed proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012, held at Thiruvananthapuram, Kerala, India, in October 2012. The 25 regular papers, 3 invited papers and 4 tool papers presented were carefully selected from numerous submissions. Conference papers are organized in 9 technical sessions, covering the topics of automata theory, logics and proofs, model checking, software verification, synthesis, verification and parallelism, probabilistic verification, constraint solving and applications, and probabilistic systems. Front Matter....Pages - Verification of Computer Switching Networks: An Overview....Pages 1-16 Dynamic Bayesian Networks: A Factored Model of Probabilistic Dynamics....Pages 17-25 Interpolant Automata....Pages 26-26 Approximating Deterministic Lattice Automata....Pages 27-41 Tight Bounds for the Determinisation and Complementation of Generalised Büchi Automata....Pages 42-56 A Succinct Canonical Register Automaton Model for Data Domains with Binary Relations....Pages 57-71 Rabinizer: Small Deterministic Automata for LTL( F , G )....Pages 72-76 The Unary Fragments of Metric Interval Temporal Logic: Bounded versus Lower Bound Constraints....Pages 77-91 On Temporal Logic and Signal Processing....Pages 92-106 Improved Single Pass Algorithms for Resolution Proof Reduction....Pages 107-121 Model Checking Systems and Specifications with Parameterized Atomic Propositions....Pages 122-136 Reachability Analysis of Polynomial Systems Using Linear Programming Relaxations....Pages 137-151 Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding....Pages 152-166 Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data....Pages 167-182 A Verifier for Functional Properties of Sequence-Manipulating Programs....Pages 183-186 Accelerating Interpolants....Pages 187-202 FunFrog: Bounded Model Checking with Interpolation-Based Function Summarization....Pages 203-207 Synthesis of Succinct Systems....Pages 208-222 Controllers with Minimal Observation Power (Application to Timed Systems)....Pages 223-237 Counterexample Guided Synthesis of Monitors for Realizability Enforcement....Pages 238-253 Parallel Assertions for Architectures with Weak Memory Models....Pages 254-268 Improved Multi-Core Nested Depth-First Search....Pages 269-283 An Experiment on Parallel Model Checking of a CTL Fragment....Pages 284-299 Variable Probabilistic Abstraction Refinement....Pages 300-316 Pareto Curves for Probabilistic Model Checking....Pages 317-332 Verification of Partial-Information Probabilistic Systems Using Counterexample-Guided Refinements....Pages 333-348 The COMICS Tool – Co mputing Mi nimal C ounterexample s for DTMCs....Pages 349-353 Computing Minimal Separating DFAs and Regular Invariants Using SAT and SMT Solvers....Pages 354-369 ALLQBF Solving by Computational Learning....Pages 370-384 Equivalence of Games with Probabilistic Uncertainty and Partial-Observation Games....Pages 385-399 A Probabilistic Kleene Theorem....Pages 400-415 Higher-Order Approximations for Verification of Stochastic Hybrid Systems....Pages 416-434 Back Matter....Pages - A book that constitutes the refereed proceedings of the 8th International Symposium on Automated Technology for Verification and Analysis, ATVA 2010, that was held in Singapore, in September 2010. It includes 3 invited talks, 21 regular papers and 9 tool papers.