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

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