Ebook: Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings

This book constitutes the thoroughly refereed proceedings of the 25th International Conference on Computer Aided Verification, CAV 2013 held in St. Petersburg, Russia in July 2013. The 54 regular and 16 tool papers presented were carefully selected from 209 submissions. The papers are organized in topical sections on biology, concurrency, hardware, hybrid systems, interpolation, loops and termination, new domains, probability and statistics, SAT and SMZ, security, shape analysis, synthesis, and time.

---

This book constitutes the thoroughly refereed proceedings of the 25th International Conference on Computer Aided Verification, CAV 2013 held in St. Petersburg, Russia in July 2013. The 54 regular and 16 tool papers presented were carefully selected from 209 submissions. The papers are organized in topical sections on biology, concurrency, hardware, hybrid systems, interpolation, loops and termination, new domains, probability and statistics, SAT and SMZ, security, shape analysis, synthesis, and time.

---

This book constitutes the thoroughly refereed proceedings of the 25th International Conference on Computer Aided Verification, CAV 2013 held in St. Petersburg, Russia in July 2013. The 54 regular and 16 tool papers presented were carefully selected from 209 submissions. The papers are organized in topical sections on biology, concurrency, hardware, hybrid systems, interpolation, loops and termination, new domains, probability and statistics, SAT and SMZ, security, shape analysis, synthesis, and time.
Content:
Front Matter....Pages -
Software Model Checking for People Who Love Automata....Pages 1-35
Multi-solver Support in Symbolic Execution....Pages 36-52
Under-Approximating Cut Sets for Reachability in Large Scale Automata Networks....Pages 53-68
Model-Checking Signal Transduction Networks through Decreasing Reachability Sets....Pages 69-84
Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking....Pages 85-100
Parameterized Verification of Asynchronous Shared-Memory Systems....Pages 101-106
Partial Orders for Efficient Bounded Model Checking of Concurrent Software....Pages 107-123
Incremental, Inductive Coverability....Pages 124-140
Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates....Pages 141-157
SVA and PSL Local Variables - A Practical Approach....Pages 158-173
Formal Verification of Hardware Synthesis....Pages 174-190
CacBDD: A BDD Package with Dynamic Cache Management....Pages 191-196
Distributed Explicit State Model Checking of Deadlock Freedom....Pages 197-212
Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems....Pages 213-228
Flow*: An Analyzer for Non-linear Hybrid Systems....Pages 229-234
Efficient Robust Monitoring for STL....Pages 235-241
Abstraction Based Model-Checking of Stability of Hybrid Systems....Pages 242-257
System Level Formal Verification via Model Checking Driven Simulation....Pages 258-263
Beautiful Interpolants....Pages 264-279
Efficient Generation of Small Interpolants in CNF....Pages 280-295
Disjunctive Interpolants for Horn-Clause Verification....Pages 296-312
Generating Non-linear Interpolants by Semidefinite Programming....Pages 313-329
Under-Approximating Loops in C Programs for Fast Counterexample Detection....Pages 330-346
Proving Termination Starting from the End....Pages 347-363
Better Termination Proving through Cooperation....Pages 364-380
Relative Equivalence in the Presence of Ambiguity....Pages 381-396
Combining Relational Learning with SMT Solvers Using CEGAR....Pages 397-412
A Fully Verified Executable LTL Model Checker....Pages 413-429
Automatic Generation of Quality Specifications....Pages 430-446
Upper Bounds for Newton’s Method on Monotone Polynomial Systems, and P-Time Model Checking of Probabilistic One-Counter Automata....Pages 447-462
Probabilistic Program Analysis with Martingales....Pages 463-478
Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties....Pages 479-494
Faster Algorithms for Markov Decision Processes with Low Treewidth....Pages 495-510
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis....Pages 511-526
Importance Splitting for Statistical Model Checking Rare Properties....Pages 527-542
Minimal Sets over Monotone Predicates in Boolean Formulae....Pages 543-558
A Scalable and Nearly Uniform Generator of SAT Witnesses....Pages 559-575
Equivalence of Extended Symbolic Finite Transducers....Pages 576-591
Finite Model Finding in SMT....Pages 592-607
ILP Modulo Theories....Pages 608-623
Smten: Automatic Translation of High-Level Symbolic Computations into SMT Queries....Pages 624-639
A Tool for Estimating Information Leakage....Pages 640-655
The TAMARIN Prover for the Symbolic Analysis of Security Protocols....Pages 656-661
QUAIL: A Quantitative Security Analyzer for Imperative Code....Pages 662-677
Lengths May Break Privacy – Or How to Check for Equivalences with Length....Pages 678-683
Finding Security Vulnerabilities in a Network Protocol Using Parameterized Systems....Pages 684-689
Fully Automated Shape Analysis Based on Forest Automata....Pages 690-695
Effectively-Propositional Reasoning about Reachability in Linked Data Structures....Pages 696-701
Automating Separation Logic Using SMT....Pages 702-707
SeLoger: A Tool for Graph-Based Reasoning in Separation Logic....Pages 708-723
Validating Library Usage Interactively....Pages 724-739
Learning Universally Quantified Invariants of Linear Data Structures....Pages 740-755
Towards Distributed Software Model-Checking Using Decision Diagrams....Pages 756-772
Automatic Abstraction in SMT-Based Unbounded Software Model Checking....Pages 773-789
DiVinE 3.0 – An Explicit-State Model Checker for Multithreaded C & C++ Programs....Pages 790-795
Solving Existentially Quantified Horn Clauses....Pages 796-812
GOAL for Games, Omega-Automata, and Logics....Pages 813-829
Program Repair without Regret....Pages 830-845
Programs from Proofs – A PCC Alternative....Pages 846-862
Recursive Program Synthesis....Pages 863-868
Efficient Synthesis for Concurrency by Semantics-Preserving Transformations....Pages 869-882
Multi-core Emptiness Checking of Timed Buchi Automata Using Inclusion Abstraction....Pages 883-889
PSyHCoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems....Pages 890-895
Lazy Abstractions for Timed Automata....Pages 896-911
Shrinktech: A Tool for the Robustness Analysis of Timed Automata....Pages 912-927
Back Matter....Pages 928-933
....Pages 934-950