Ebook: Automated Technology for Verification and Analysis: 10th International Symposium, ATVA 2012, Thiruvananthapuram, India, October 3-6, 2012. Proceedings

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.

---

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.

---

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.
Content:
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 – Computing Minimal Counterexamples 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 -

---

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.
Content:
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 – Computing Minimal Counterexamples 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 -
....