Computer Aided Verification: 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings

Front Matter....Pages -
Transactional Memory: Glimmer of a Theory....Pages 1-15
Mixed-Signal System Verification: A High-Speed Link Example....Pages 16-16
Modelling Epigenetic Information Maintenance: A Kappa Tutorial....Pages 17-32
Component-Based Construction of Real-Time Systems in BIP....Pages 33-34
Models and Proofs of Protocol Security: A Progress Report....Pages 35-49
Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after?....Pages 50-50
SPEED: Symbolic Complexity Bound Analysis....Pages 51-62
Regression Verification: Proving the Equivalence of Similar Programs....Pages 63-63
Symbolic Counter Abstraction for Concurrent Software....Pages 64-78
Priority Scheduling of Distributed Systems Based on Model Checking....Pages 79-93
Explaining Counterexamples Using Causality....Pages 94-108
Size-Change Termination, Monotonicity Constraints and Ranking Functions....Pages 109-123
Linear Functional Fixed-points....Pages 124-139
Better Quality in Synthesis through Quantitative Objectives....Pages 140-156
Automatic Verification of Integer Array Programs....Pages 157-172
Automated Analysis of Java Methods for Confidentiality....Pages 173-187
Requirements Validation for Hybrid Systems....Pages 188-203
Towards Performance Prediction of Compositional Models in Industrial GALS Designs....Pages 204-218
Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion....Pages 219-232
Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers....Pages 233-247
Meta-analysis for Atomicity Violations under Nested Locking....Pages 248-262
An Antichain Algorithm for LTL Realizability....Pages 263-277
On Extending Bounded Proofs to Inductive Proofs....Pages 278-290
Games through Nested Fixpoints....Pages 291-305
Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories....Pages 306-320
Software Transactional Memory on Relaxed Memory Models....Pages 321-336
Sliding Window Abstraction for Infinite Markov Chains....Pages 337-352
Centaur Technology Media Unit Verification....Pages 353-367
Incremental Instance Generation in Local Reasoning....Pages 368-382
Quantifier Elimination via Functional Composition....Pages 383-397
Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique....Pages 398-413
Replacing Testing with Formal Verification in Intel $^{\\scriptsize\\circledR}$ Core TM i7 Processor Execution Engine Validation....Pages 414-429
Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models....Pages 430-445
A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints....Pages 446-461
Generalizing DPLL to Richer Logics....Pages 462-476
Reducing Context-Bounded Concurrent Reachability to Sequential Reachability....Pages 477-492
Intra-module Inference....Pages 493-508
Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers....Pages 509-524
Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints....Pages 525-539
Reachability Analysis of Hybrid Systems Using Support Functions....Pages 540-554
Reducing Test Inputs Using Information Partitions....Pages 555-569
On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure....Pages 570-583
Cardinality Abstraction for Declarative Networking Applications....Pages 584-598
Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences....Pages 599-613
D-Finder: A Tool for Compositional Deadlock Detection and Verification....Pages 614-619
HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment....Pages 620-626
The Zonotope Abstract Domain Taylor1+....Pages 627-633
InvGen: An Efficient Invariant Generator....Pages 634-640
INFAMY: An Infinite-State Markov Model Checker....Pages 641-647
Browser-Based Enforcement of Interface Contracts in Web Applications with BeepBeep....Pages 648-653
 Homer : A Higher-Order Observational Equivalence Model checkER....Pages 654-660
 Apron : A Library of Numerical Abstract Domains for Static Analysis....Pages 661-667
Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic....Pages 668-674
 CalFuzzer : An Extensible Active Testing Framework for Concurrent Programs....Pages 675-681
MCMAS: A Model Checker for the Verification of Multi-Agent Systems....Pages 682-688
TASS: Timing Analyzer of Scenario-Based Specifications....Pages 689-695
Translation Validation: From Simulink to C....Pages 696-701
VS 3 : SMT Solvers for Program Verification....Pages 702-708
PAT: Towards Flexible Verification under Fairness....Pages 709-714
A Concurrent Portfolio Approach to SMT Solving....Pages 715-720
Back Matter....Pages -