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

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Bouajjani, Ahmed (Επιμελητής έκδοσης), Maler, Oded (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg, 2009.
• Σειρά: Lecture Notes in Computer Science, 5643
• Θέματα: Computer science.; Architecture, Computer.; Software engineering.; Computer programming.; Computer logic.; Mathematical logic.; Computer Science.; Programming Techniques.; Computer System Implementation.; Software Engineering/Programming and Operating Systems.; Logics and Meanings of Programs.; Software Engineering.; Mathematical Logic and Formal Languages.

This book constitutes the refereed proceedings of the 21st International Conference on Computer Aided Verification, CAV 2009, held in Grenoble, France, in June/July 2009. The 36 revised full papers presented together with 16 tool papers and 4 invited talks and 4 invited tutorials were carefully revi...

Πίνακας περιεχομένων:

• Invited Tutorials
• Transactional Memory: Glimmer of a Theory
• Mixed-Signal System Verification: A High-Speed Link Example
• Modelling Epigenetic Information Maintenance: A Kappa Tutorial
• Component-Based Construction of Real-Time Systems in BIP
• Invited Talks
• Models and Proofs of Protocol Security: A Progress Report
• Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after?
• SPEED: Symbolic Complexity Bound Analysis
• Regression Verification: Proving the Equivalence of Similar Programs
• Regular Papers
• Symbolic Counter Abstraction for Concurrent Software
• Priority Scheduling of Distributed Systems Based on Model Checking
• Explaining Counterexamples Using Causality
• Size-Change Termination, Monotonicity Constraints and Ranking Functions
• Linear Functional Fixed-points
• Better Quality in Synthesis through Quantitative Objectives
• Automatic Verification of Integer Array Programs
• Automated Analysis of Java Methods for Confidentiality
• Requirements Validation for Hybrid Systems
• Towards Performance Prediction of Compositional Models in Industrial GALS Designs
• Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion
• Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
• Meta-analysis for Atomicity Violations under Nested Locking
• An Antichain Algorithm for LTL Realizability
• On Extending Bounded Proofs to Inductive Proofs
• Games through Nested Fixpoints
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Software Transactional Memory on Relaxed Memory Models
• Sliding Window Abstraction for Infinite Markov Chains
• Centaur Technology Media Unit Verification
• Incremental Instance Generation in Local Reasoning
• Quantifier Elimination via Functional Composition
• Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique
• Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation
• Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models
• A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints
• Generalizing DPLL to Richer Logics
• Reducing Context-Bounded Concurrent Reachability to Sequential Reachability
• Intra-module Inference
• Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers
• Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints
• Reachability Analysis of Hybrid Systems Using Support Functions
• Reducing Test Inputs Using Information Partitions
• On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure
• Cardinality Abstraction for Declarative Networking Applications
• Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences
• Tool Papers
• D-Finder: A Tool for Compositional Deadlock Detection and Verification
• HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment
• The Zonotope Abstract Domain Taylor1+
• InvGen: An Efficient Invariant Generator
• INFAMY: An Infinite-State Markov Model Checker
• Browser-Based Enforcement of Interface Contracts in Web Applications with BeepBeep
• Homer: A Higher-Order Observational Equivalence Model checkER
• Apron: A Library of Numerical Abstract Domains for Static Analysis
• Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic
• CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs
• MCMAS: A Model Checker for the Verification of Multi-Agent Systems
• TASS: Timing Analyzer of Scenario-Based Specifications
• Translation Validation: From Simulink to C
• VS3: SMT Solvers for Program Verification
• PAT: Towards Flexible Verification under Fairness
• A Concurrent Portfolio Approach to SMT Solving.