Coverart for item
The Resource Computer aided verification : 10th International Conference, CAV'98, Vancouver, BC, Canada, June 28 - July 2, 1998 ; proceedings, Alan J. Hu, Moshe Y. Vardi (eds.)

Computer aided verification : 10th International Conference, CAV'98, Vancouver, BC, Canada, June 28 - July 2, 1998 ; proceedings, Alan J. Hu, Moshe Y. Vardi (eds.)

Label
Computer aided verification : 10th International Conference, CAV'98, Vancouver, BC, Canada, June 28 - July 2, 1998 ; proceedings
Title
Computer aided verification
Title remainder
10th International Conference, CAV'98, Vancouver, BC, Canada, June 28 - July 2, 1998 ; proceedings
Statement of responsibility
Alan J. Hu, Moshe Y. Vardi (eds.)
Creator
Contributor
Subject
Genre
Language
eng
Summary
This book consitutes the refereed proceedings of the 10th International Conference on Computer Aided Verification, CAV'98, held in Vancouver, BC, Canada, in June/July 1998. The 33 revised full papers and 10 tool papers presented were carefully selected from a total of 117 submissions. Also included are 11 invited contributions. Among the topics covered are modeling and specification formalisms; verification techniques like state-space exploration, model checking, synthesis, and automated deduction; various verification techniques; applications and case studies, and verification in practice
Member of
Cataloging source
SCPER
Dewey number
004.24
Illustrations
illustrations
Index
index present
LC call number
QA76.76.V47
LC item number
C38 1998
Literary form
non fiction
http://bibfra.me/vocab/lite/meetingDate
1998
http://bibfra.me/vocab/lite/meetingName
CAV (Conference)
Nature of contents
  • dictionaries
  • bibliography
http://library.link/vocab/relatedWorkOrContributorName
  • Hu, Alan J.
  • Vardi, Moshe Y
Series statement
Lecture notes in computer science,
Series volume
1427
http://library.link/vocab/subjectName
  • Computer software
  • Integrated circuits
  • Computer software
  • Integrated circuits
  • Verificatie
  • Software
Label
Computer aided verification : 10th International Conference, CAV'98, Vancouver, BC, Canada, June 28 - July 2, 1998 ; proceedings, Alan J. Hu, Moshe Y. Vardi (eds.)
Instantiates
Publication
Bibliography note
Includes bibliographical references and index
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
Synchronous programming of reactive systems -- Ten years of partial order reduction -- An ACL2 proof of write invalidate cache coherence -- Transforming the theorem prover into a digital design tool: From concept car to off-road vehicle -- A role for theorem proving in multi-processor design -- A formal method experience at secure computing corporation -- Formal methods in an industrial environment -- On checking model checkers -- Finite-state analysis of security protocols -- Integrating proof-based and model-checking techniques for the formal verification of cryptographic protocols -- Verifying systems with infinite but regular state spaces -- Formal verification of out-of-order execution using incremental flushing -- Verification of an implementation of Tomasulo's algorithm by compositional model checking -- Decomposing the proof of correctness of pipelined microprocessors -- Processor verification with precise exceptions and speculative execution -- Symmetry reductions in model checking -- Structural symmetry and model checking -- Using magnetic disk instead of main memory in the Mur? verifier -- On-the-fly model checking of RCTL formulas -- From pre-historic to post-modern symbolic model checking -- Model checking LTL using net unforldings -- Model checking for a first-order temporal logic using multiway decision graphs -- On the limitations of ordered representations of functions -- BDD based procedures for a theory of equality with uninterpreted functions -- Computing reachable control states of systems modeled with uninterpreted functions and infinite memory -- Multiple counters automata, safety analysis and presburger arithmetic -- A comparison of Presburger engines for EFSM reachability -- Generating finite-state abstractions of reactive systems using decision procedures -- On-the-fly analysis of systems with unbounded, lossy FIFO channels -- Computing abstractions of infinite state systems compositionally and automatically -- Normed simulations -- An experiment in parallelizing an application using formal methods -- Efficient symbolic detection of global properties in distributed systems -- A machine-checked proof of the optimality of a real-time scheduling policy -- A general approach to partial order reductions in symbolic verification -- Correctness of the concurrent approach to symbolic verification of interleaved models -- Verification of timed systems using POSETs -- Mechanising BAN Kerberos by the inductive method -- Protocol verification in Nuprl -- You assume, we guarantee: Methodology and case studies -- Verification of a parameterized bus arbitration protocol -- The 'test model-checking' approach to the verification of formal memory models of multiprocessors -- Design constraints in symbolic model checking -- Verification of floating-point adders -- Xeve, an Esterel verification environment -- InVeSt : A tool for the verification of invariants -- Verifying mobile processes in the HAL environment -- MONA 1.x: New techniques for WS1S and WS2S -- MOCHA: Modularity in model checking -- SCR: A toolset for specifying and analyzing software requirements -- A toolset for message sequence charts -- Real-time verification of Statemate designs -- Optikron: A tool suite for enhancing model-checking of real-time systems -- Kronos: A model-checking tool for real-time systems
Control code
321283648
Dimensions
unknown
Extent
1 online resource (ix, 552 pages)
Form of item
online
Isbn
9783540693390
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Other control number
10.1007/BFb0028725
Other physical details
illustrations.
Sound
unknown sound
Specific material designation
remote
System control number
(OCoLC)321283648
Label
Computer aided verification : 10th International Conference, CAV'98, Vancouver, BC, Canada, June 28 - July 2, 1998 ; proceedings, Alan J. Hu, Moshe Y. Vardi (eds.)
Publication
Bibliography note
Includes bibliographical references and index
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
Synchronous programming of reactive systems -- Ten years of partial order reduction -- An ACL2 proof of write invalidate cache coherence -- Transforming the theorem prover into a digital design tool: From concept car to off-road vehicle -- A role for theorem proving in multi-processor design -- A formal method experience at secure computing corporation -- Formal methods in an industrial environment -- On checking model checkers -- Finite-state analysis of security protocols -- Integrating proof-based and model-checking techniques for the formal verification of cryptographic protocols -- Verifying systems with infinite but regular state spaces -- Formal verification of out-of-order execution using incremental flushing -- Verification of an implementation of Tomasulo's algorithm by compositional model checking -- Decomposing the proof of correctness of pipelined microprocessors -- Processor verification with precise exceptions and speculative execution -- Symmetry reductions in model checking -- Structural symmetry and model checking -- Using magnetic disk instead of main memory in the Mur? verifier -- On-the-fly model checking of RCTL formulas -- From pre-historic to post-modern symbolic model checking -- Model checking LTL using net unforldings -- Model checking for a first-order temporal logic using multiway decision graphs -- On the limitations of ordered representations of functions -- BDD based procedures for a theory of equality with uninterpreted functions -- Computing reachable control states of systems modeled with uninterpreted functions and infinite memory -- Multiple counters automata, safety analysis and presburger arithmetic -- A comparison of Presburger engines for EFSM reachability -- Generating finite-state abstractions of reactive systems using decision procedures -- On-the-fly analysis of systems with unbounded, lossy FIFO channels -- Computing abstractions of infinite state systems compositionally and automatically -- Normed simulations -- An experiment in parallelizing an application using formal methods -- Efficient symbolic detection of global properties in distributed systems -- A machine-checked proof of the optimality of a real-time scheduling policy -- A general approach to partial order reductions in symbolic verification -- Correctness of the concurrent approach to symbolic verification of interleaved models -- Verification of timed systems using POSETs -- Mechanising BAN Kerberos by the inductive method -- Protocol verification in Nuprl -- You assume, we guarantee: Methodology and case studies -- Verification of a parameterized bus arbitration protocol -- The 'test model-checking' approach to the verification of formal memory models of multiprocessors -- Design constraints in symbolic model checking -- Verification of floating-point adders -- Xeve, an Esterel verification environment -- InVeSt : A tool for the verification of invariants -- Verifying mobile processes in the HAL environment -- MONA 1.x: New techniques for WS1S and WS2S -- MOCHA: Modularity in model checking -- SCR: A toolset for specifying and analyzing software requirements -- A toolset for message sequence charts -- Real-time verification of Statemate designs -- Optikron: A tool suite for enhancing model-checking of real-time systems -- Kronos: A model-checking tool for real-time systems
Control code
321283648
Dimensions
unknown
Extent
1 online resource (ix, 552 pages)
Form of item
online
Isbn
9783540693390
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Other control number
10.1007/BFb0028725
Other physical details
illustrations.
Sound
unknown sound
Specific material designation
remote
System control number
(OCoLC)321283648

Library Locations

    • Ellis LibraryBorrow it
      1020 Lowry Street, Columbia, MO, 65201, US
      38.944491 -92.326012
Processing Feedback ...