Cantitate/Preț
Produs
Total produse
Vezi coșul
Computer Aided Verification: 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009, Proceedings de Ahmed Bouajjani

Computer Aided Verification: 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009, Proceedings: Lecture Notes in Computer Science, cartea 5643

Editat de Ahmed Bouajjani, Oded Maler
en Limba Engleză Paperback – 19 iun 2009
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 reviewed and selected from 135 regular paper and 34 tool paper submissions. The papers are dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems; their scope ranges from theoretical results to concrete applications, with an emphasis on practical verification tools and the underlying algorithms and techniques.
Citește tot Restrânge

Din seria Lecture Notes in Computer Science

Preț: 65619 lei

Preț vechi: 82023 lei
-20% Nou

Puncte Express: 984
Preț estimativ în valută:
12558€ • 13083$ • 10441£

Carte tipărită la comandă

Livrare economică 11-25 februarie 25

 Adaugă în coș

Wish list
Gift list
Am citit!
Adaugă în listă
Preluare comenzi: 021 569.72.76

Specificații

ISBN-13: 9783642026577
ISBN-10: 3642026575
Pagini: 740
Ilustrații: XV, 722 p.
Dimensiuni: 155 x 235 x 39 mm
Greutate: 1.02 kg
Ediția:2009
Editura: Springer Berlin, Heidelberg
Colecția Springer
Seriile Lecture Notes in Computer Science, Theoretical Computer Science and General Issues

Locul publicării:Berlin, Heidelberg, Germany

Public țintă

Research

Cuprins

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 CoreTMi7 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 Programswithin 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.

Textul de pe ultima copertă

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 reviewed and selected from 135 regular paper and 34 tool paper submissions. The papers are dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems; their scope ranges from theoretical results to concrete applications, with an emphasis on practical verification tools and the underlying algorithms and techniques.