Computer Aided Verification de Rajeev Alur

Computer Aided Verification: 8th International Conference, CAV '96, New Brunswick, NJ, USA, July 31 - August 3, 1996. Proceedings: Lecture Notes in Computer Science, cartea 1102

Rajeev Alur

Thomas Henzinger

en Limba Engleză Paperback – 17 iul 1996

This book constitutes the refereed proceedings of the 8th International Conference on Computer Aided Verification, CAV '96, held in New Brunswick, NJ, USA, in July/August 1996 as part of the FLoC '96 federated conference.
The volume presents 32 revised full research contributions selected from a total of 93 submissions; also included are 20 carefully selected descriptions of tools and case studies. The set of papers reports the state-of-the-art of the theory and practice of computer assisted formal analysis methods for software and hardware systems; a certain emphasis is placed on verification tools and the algorithms and techniques that are needed for their implementation.

Citește tot Restrânge

Din seria Lecture Notes in Computer Science

20%

Preț: 1061^.55 lei
20%

Preț: 307^.71 lei
20%

Preț: 438^.69 lei
20%

Preț: 645^.28 lei
Preț: 410^.88 lei
15%

Preț: 580^.46 lei
17%

Preț: 427^.22 lei
20%

Preț: 596^.46 lei
Preț: 381^.21 lei
20%

Preț: 353^.50 lei
20%

Preț: 1414^.79 lei
20%

Preț: 309^.90 lei
20%

Preț: 583^.40 lei
20%

Preț: 1075^.26 lei
20%

Preț: 310^.26 lei
20%

Preț: 655^.02 lei
20%

Preț: 580^.93 lei
20%

Preț: 340^.32 lei
15%

Preț: 438^.59 lei
20%

Preț: 591^.51 lei
20%

Preț: 649^.49 lei
20%

Preț: 337^.00 lei
Preț: 449^.57 lei
20%

Preț: 607^.39 lei
20%

Preț: 1024^.44 lei
20%

Preț: 579^.30 lei
20%

Preț: 763^.23 lei
20%

Preț: 453^.32 lei
20%

Preț: 575^.48 lei
20%

Preț: 585^.88 lei
20%

Preț: 825^.93 lei
20%

Preț: 763^.23 lei
17%

Preț: 360^.19 lei
20%

Preț: 1183^.14 lei
20%

Preț: 340^.32 lei
20%

Preț: 504^.57 lei
20%

Preț: 369^.12 lei
20%

Preț: 583^.40 lei
20%

Preț: 343^.62 lei
20%

Preț: 350^.21 lei
20%

Preț: 764^.89 lei
20%

Preț: 583^.40 lei
Preț: 389^.48 lei
20%

Preț: 341^.95 lei
20%

Preț: 238^.01 lei
20%

Preț: 538^.29 lei

Cuprins

Symbolic verification of communication protocols with infinite state spaces using QDDs.- A conjunctively decomposed boolean representation for symbolic model checking.- Symbolic model checking using algebraic geometry.- A partition refinement algorithm for the ?-calculus.- Polynomial time algorithms for testing probabilistic bisimulation and simulation.- Pushdown processes: Games and model checking.- Module checking.- Automatic verification of parameterized synchronous systems.- HORNSAT, model checking, verification and games.- Verifying the SRT division algorithm using theorem proving techniques.- Modular verification of SRT division.- Mechanically verifying a family of multiplier circuits.- Verifying systems with replicated components in mur?.- Verification of arithmetic circuits by comparing two similar circuits.- Automated deduction and formal methods.- A platform for combining deductive with algorithmic verification.- Verifying invariants using theorem proving.- Deductive model checking.- Automated verification by induction with associative-commutative operators.- Analysis of timed systems based on time-abstracting bisimulations.- Verification of an Audio Protocol with bus collision using Uppaal.- Selective quantitative analysis and interval model checking: Verifying different facets of a system.- Verifying continuous time Markov chains.- Verifying safety properties of differential equations.- Temporal verification by diagram transformations.- Protocol verification by aggregation of distributed transactions.- Atomicity refinement and trace reduction theorems.- Powerful techniques for the automatic generation of invariants.- Saving space by fully exploiting invisible transitions.- Using on-the-fly verification techniques for the generation of test suites.- Automatic translation of natural language system specifications into temporal logic.- Verification of fair transition systems.- The state of Spin.- The Mur ? verification system.- The NCSU Concurrency Workbench.- The Concurrency Factory: A development environment for concurrent systems.- XVERSA: An integrated graphical and textual toolset for the specification and analysis of resource-bound real-time systems.- EVP: Integration of FDTs for the analysis and verification of communication protocols.- PVS: Combining specification, proof checking, and model checking.- STeP: Deductive-algorithmic verification of reactive and real-time systems.- Symbolic model checking.- COSPAN.- VIS: A system for verification and synthesis.- MDG tools for the verification of RTL designs.- CADP a protocol validation and verification toolbox.- The FC2TOOLS set.- The Real-Time Graphical Interval Logic toolset.- The METAFrame'95 environment.- Verification Support Environment.- Marrella: A tool for simulation and verification.- Verifying the safety of a practical concurrent garbage collector.- Verification by behaviour abstraction.