Lecture Notes in Computer Science

9th International Conference, CAV'97, Haifa, Israel, June 22-25, 1997, Proceedings

By: Orna Grumberg (Editor)

Write A Review

Paperback | 4 June 1997

At a Glance

Paperback
504 Pages

Dimensions(cm)
22.86 x 16.51 x 1.91

Paperback

$84.99

or 4 interest-free payments of $21.25 with

Ships in 5 to 7 business days

This book constitutes the strictly refereed proceedings of the 9th International Conference on Computer Aided Verification, CAV '97, held in Haifa, Israel, in June 1997.
The volume presents 34 revised full papers selected from a total of 84 submissions. Also included are 7 invited contributions as well as 12 tool descriptions. The volume is dedicated to the theory and practice of computer aided formal methods for software and hardware verification, with an emphasis on verification tools and algorithms and the techniques needed for their implementation. The book is a unique record documenting the recent progress in the area.

Shipping

	Standard Shipping	Express Shipping
Metro postcodes:	$9.99	$14.95
Regional postcodes:	$9.99	$14.95
Rural postcodes:	$9.99	$14.95

Orders over $89.00 qualify for free shipping.

How to return your order

At Booktopia, we offer hassle-free returns in accordance with our returns policy. If you wish to return an item, please get in touch with Booktopia Customer Care.

Additional postage charges may be applicable.

Defective items

If there is a problem with any of the items received for your order then the Booktopia Customer Care team is ready to assist you.

For more info please visit our Help Centre.

You Can Find This Book In

Non-Fiction Computing & I.T.Computer Programming & Software Development Software Engineering Software Testing & Verification Computer Science Computer Architecture & Logic Design Systems Analysis & Design Mathematics Mathematical Foundation Mathematical Logic Artificial Intelligence

Expert Systems & Knowledge-Based Systems

Practical challenges for industrial formal verification tools	p. 1
Formal verification of digital systems, from ASICs to HW/SW codesign - a pragmatic approach	p. 3
The industrial success of verification tools based on Stalmarck's method	p. 7
Formal verification - application and case studies	p. 11
Automatic abstraction techniques for propositional mu-calculus model checking	p. 12
A compositional rule for hardware design refinement	p. 24
Module checking revisited	p. 36
Using compositional preorders in the verification of sliding window protocol	p. 48
An efficient decision procedure for the theory of fixed-sized bit-vectors	p. 60
Construction of abstract state graphs with PVS	p. 72
Verification of a chemical process leak test procedure	p. 84
Automatic datapath extraction for efficient usage of HDD	p. 95
An n log n algorithm for online BDD refinement	p. 107
Weak bisimulation for fully probabilistic processes	p. 119
Towards a mechanization of cryptographic protocol verification	p. 131
Efficient model checking using tabled resolution	p. 143
Containment of regular languages in non-regular timing diagram languages is decidable	p. 155
An improved reachability analysis method for strongly linear hybrid systems	p. 167
Some progress in the symbolic verification of timed automata	p. 179
STARI: A case study in compositional and hierarchical timing verification	p. 191
A provably correct embedded verifier for the certification of safety critical software	p. 202
Model checking in a microprocessor design project	p. 214
Some thoughts on statecharts, 13 years later	p. 226
On-the-fly model checking under fairness that exploits symmetry	p. 232
Exploiting symmetry when verifying transistor-level circuits by symbolic trajectory evaluation	p. 244
Parallelizing the Murphi verifier	p. 256
A new heuristic for bad cycle detection using BDDs	p. 268
Efficient detection of vacuity in ACTL formulas	p. 279
Model checking and transitive-closure logic	p. 291
Boolean and 2-adic numbers based techniques for verifying synchronous designs	p. 303
Programs with quasi-stable channels are effectively recognizable	p. 304
Combining constraint solving and symbolic model checking for a class of systems with non-linear constraints	p. 316
Relaxed visibility enhances partial order reduction	p. 328
Partial-order reduction in symbolic state space exploration	p. 340
Deadlock checking using net unfoldings	p. 352
Trace table based approach for pipelined microprocessor verification	p. 364
On combining formal and informal verification	p. 376
Efficient modeling of memory arrays in symbolic simulation	p. 388
Symbolic model checking of infinite state systems using Presburger arithmetic	p. 400
Parametrized verification of linear networks using automata as invariants	p. 412
Symbolic model checking with rich assertional languages	p. 424
The Invariant Checker: Automated deductive verification of reactive systems	p. 436
The PEP tool	p. 440
TermiLog: A system for checking termination of queries to logic programs	p. 444
MOSEL: A sound and efficient tool for M2L(Str)	p. 448
The Verus Tool: A quantitative approach to the formal verification of real-time systems	p. 452
UPPAAL - Status and developments	p. 456
HYTECH: A model checker for hybrid systems	p. 460
SMC: A symmetry based model checker for verification of liveness properties	p. 464
mucke - efficient mu-calculus model checking	p. 468
prod 3.2 - An advanced tool for efficient reachability analysis	p. 472
VeriSoft: A tool for the automatic analysis of concurrent reactive software	p. 476
RuleBase: Model checking at IBM	p. 480
Author Index	p. 485
Table of Contents provided by Blackwell. All Rights Reserved.

Lecture Notes in Computer Science

9th International Conference, CAV'97, Haifa, Israel, June 22-25, 1997, Proceedings

At a Glance

Paperback

Shipping

How to return your order

Defective items

You Can Find This Book In

More in Artificial Intelligence

The God We Made

The Threat and Promise of Artificial Intelligence; Quarterly Essay 102

The New Age of Sexism

How the AI Revolution is Reinventing Misogyny

If Anyone Builds It, Everyone Dies

The Case Against Superintelligent AI

How We Learn

The New Science of Education and the Brain

The Infinity Machine

Demis Hassabis, DeepMind and the Quest for Superintelligence

CEH Certified Ethical Hacker v13 Study Guide

Sybex Study Guide

Co-Intelligence

Living and Working with AI

Contemporary Strategic Business Transformation

AI Frontiers

Federated Learning for Healthcare

Applications with Case Studies

Natural Language Processing and Artificial Intelligence

A Perspective Towards Current Trends, Challenges, and Applications

Robo-Advisors and Artificial Intelligence in Human Resources Management

Revolutionizing HR

Artificial Intelligence

A Modern Approach, 4th Global Edition

Control, Robotics and Sensors

Design, Control and Applications

AI for Public Relations

A How-To Guide for Implementation and Management

Navigating the AI Frontier in Business

Balancing Economy, Ecology, and Inclusion

The Cambridge Handbook of AI in Civil Dispute Resolution

Cambridge Law Handbooks

We Are As Gods

A Survival Guide for the Age of Abundance

AI and Data Science in Medical Research

New Developments and Advances

Machine Learning for Spatial Environmental Data

Theory, Applications and Software

Proceedings of the 6th International Conference on Big Data Analytics for Cyber-Physical System in Smart City, Volume 1

BDCPS 2024, December 7-8, Ji'an, China

Digital Transformation: What Kind of Smart Life do we have today?

Volume 1

Research and Education in Urban History in the Age of Digital Libraries

4th International Workshop, UHDL 2025, Vienna, Austria, November 3-5, 2025, Revised Selected Papers

Enhancing Ultra-Low-Field MRI with Paired High-Field MRI Comparisons for Brain Imaging

First International Challenge, ULF-EnC 2025, Held in Conjunction with MICCAI 2025, Daejeon, South Korea, September 23, 2025, Proceedings

Translate

Multilingual Access to Critical Services in the Age of AI

This product is categorised by