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.)
Resource Information
The item Computer aided verification : 10th International Conference, CAV'98, Vancouver, BC, Canada, June 28  July 2, 1998 ; proceedings, Alan J. Hu, Moshe Y. Vardi (eds.) represents a specific, individual, material embodiment of a distinct intellectual or artistic creation found in University of Missouri Libraries.This item is available to borrow from 1 library branch.
Resource Information
The item Computer aided verification : 10th International Conference, CAV'98, Vancouver, BC, Canada, June 28  July 2, 1998 ; proceedings, Alan J. Hu, Moshe Y. Vardi (eds.) represents a specific, individual, material embodiment of a distinct intellectual or artistic creation found in University of Missouri Libraries.
This item is available to borrow from 1 library branch.
 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 statespace exploration, model checking, synthesis, and automated deduction; various verification techniques; applications and case studies, and verification in practice
 Language
 eng
 Extent
 1 online resource (ix, 552 pages)
 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 offroad vehicle
 A role for theorem proving in multiprocessor design
 A formal method experience at secure computing corporation
 Formal methods in an industrial environment
 On checking model checkers
 Finitestate analysis of security protocols
 Integrating proofbased and modelchecking techniques for the formal verification of cryptographic protocols
 Verifying systems with infinite but regular state spaces
 Formal verification of outoforder 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
 Onthefly model checking of RCTL formulas
 From prehistoric to postmodern symbolic model checking
 Model checking LTL using net unforldings
 Model checking for a firstorder 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 finitestate abstractions of reactive systems using decision procedures
 Onthefly 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 machinechecked proof of the optimality of a realtime 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 modelchecking' approach to the verification of formal memory models of multiprocessors
 Design constraints in symbolic model checking
 Verification of floatingpoint 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
 Realtime verification of Statemate designs
 Optikron: A tool suite for enhancing modelchecking of realtime systems
 Kronos: A modelchecking tool for realtime systems
 Isbn
 9783540693390
 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.)
 Subject

 Computer software  Verification
 Computer software  Verification  Congresses
 Conference papers and proceedings
 Conference papers and proceedings
 Congressen (vorm)
 Integrated circuits  Verification
 Integrated circuits  Verification
 Integrated circuits  Verification  Congresses
 Software
 Verificatie
 Computer software  Verification
 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 statespace exploration, model checking, synthesis, and automated deduction; various verification techniques; applications and case studies, and verification in practice
 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.)
 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 offroad vehicle  A role for theorem proving in multiprocessor design  A formal method experience at secure computing corporation  Formal methods in an industrial environment  On checking model checkers  Finitestate analysis of security protocols  Integrating proofbased and modelchecking techniques for the formal verification of cryptographic protocols  Verifying systems with infinite but regular state spaces  Formal verification of outoforder 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  Onthefly model checking of RCTL formulas  From prehistoric to postmodern symbolic model checking  Model checking LTL using net unforldings  Model checking for a firstorder 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 finitestate abstractions of reactive systems using decision procedures  Onthefly 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 machinechecked proof of the optimality of a realtime 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 modelchecking' approach to the verification of formal memory models of multiprocessors  Design constraints in symbolic model checking  Verification of floatingpoint 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  Realtime verification of Statemate designs  Optikron: A tool suite for enhancing modelchecking of realtime systems  Kronos: A modelchecking tool for realtime 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.)
 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 offroad vehicle  A role for theorem proving in multiprocessor design  A formal method experience at secure computing corporation  Formal methods in an industrial environment  On checking model checkers  Finitestate analysis of security protocols  Integrating proofbased and modelchecking techniques for the formal verification of cryptographic protocols  Verifying systems with infinite but regular state spaces  Formal verification of outoforder 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  Onthefly model checking of RCTL formulas  From prehistoric to postmodern symbolic model checking  Model checking LTL using net unforldings  Model checking for a firstorder 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 finitestate abstractions of reactive systems using decision procedures  Onthefly 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 machinechecked proof of the optimality of a realtime 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 modelchecking' approach to the verification of formal memory models of multiprocessors  Design constraints in symbolic model checking  Verification of floatingpoint 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  Realtime verification of Statemate designs  Optikron: A tool suite for enhancing modelchecking of realtime systems  Kronos: A modelchecking tool for realtime 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
Subject
 Computer software  Verification
 Computer software  Verification  Congresses
 Conference papers and proceedings
 Conference papers and proceedings
 Congressen (vorm)
 Integrated circuits  Verification
 Integrated circuits  Verification
 Integrated circuits  Verification  Congresses
 Software
 Verificatie
 Computer software  Verification
Genre
Member of
Library Links
Embed
Settings
Select options that apply then copy and paste the RDF/HTML data fragment to include in your application
Embed this data in a secure (HTTPS) page:
Layout options:
Include data citation:
<div class="citation" vocab="http://schema.org/"><i class="fa faexternallinksquare fafw"></i> Data from <span resource="http://link.library.missouri.edu/portal/Computeraidedverification10thInternational/xiSZePsykyo/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.library.missouri.edu/portal/Computeraidedverification10thInternational/xiSZePsykyo/">Computer aided verification : 10th International Conference, CAV'98, Vancouver, BC, Canada, June 28  July 2, 1998 ; proceedings, Alan J. Hu, Moshe Y. Vardi (eds.)</a></span>  <span property="potentialAction" typeOf="OrganizeAction"><span property="agent" typeof="LibrarySystem http://library.link/vocab/LibrarySystem" resource="http://link.library.missouri.edu/"><span property="name http://bibfra.me/vocab/lite/label"><a property="url" href="http://link.library.missouri.edu/">University of Missouri Libraries</a></span></span></span></span></div>
Note: Adjust the width and height settings defined in the RDF/HTML code fragment to best match your requirements
Preview
Cite Data  Experimental
Data Citation of the Item Computer aided verification : 10th International Conference, CAV'98, Vancouver, BC, Canada, June 28  July 2, 1998 ; proceedings, Alan J. Hu, Moshe Y. Vardi (eds.)
Copy and paste the following RDF/HTML data fragment to cite this resource
<div class="citation" vocab="http://schema.org/"><i class="fa faexternallinksquare fafw"></i> Data from <span resource="http://link.library.missouri.edu/portal/Computeraidedverification10thInternational/xiSZePsykyo/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.library.missouri.edu/portal/Computeraidedverification10thInternational/xiSZePsykyo/">Computer aided verification : 10th International Conference, CAV'98, Vancouver, BC, Canada, June 28  July 2, 1998 ; proceedings, Alan J. Hu, Moshe Y. Vardi (eds.)</a></span>  <span property="potentialAction" typeOf="OrganizeAction"><span property="agent" typeof="LibrarySystem http://library.link/vocab/LibrarySystem" resource="http://link.library.missouri.edu/"><span property="name http://bibfra.me/vocab/lite/label"><a property="url" href="http://link.library.missouri.edu/">University of Missouri Libraries</a></span></span></span></span></div>