000  05976nam a22006015i 4500  

001  9783540693390  
003  DEHe213  
005  20170515111459.0  
007  cr nn 008mamaa  
008  121227s1998 gw  s  0eng d  
020 
_a9783540693390 _99783540693390 

024  7 
_a10.1007/BFb0028725 _2doi 

050  4  _aQA76.758  
072  7 
_aUMZ _2bicssc 

072  7 
_aUL _2bicssc 

072  7 
_aCOM051230 _2bisacsh 

082  0  4 
_a005.1 _223 
245  1  0 
_aComputer Aided Verification _h[electronic resource] : _b10th International Conference, CAV'98 Vancouver, BC, Canada, June 28 – July 2, 1998 Proceedings / _cedited by Alan J. Hu, Moshe Y. Vardi. 
264  1 
_aBerlin, Heidelberg : _bSpringer Berlin Heidelberg, _c1998. 

300 
_aX, 552 p. _bonline resource. 

336 
_atext _btxt _2rdacontent 

337 
_acomputer _bc _2rdamedia 

338 
_aonline resource _bcr _2rdacarrier 

347 
_atext file _bPDF _2rda 

490  1 
_aLecture Notes in Computer Science, _x03029743 ; _v1427 

505  0  _aSynchronous 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.  
520  _aThis 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.  
650  0  _aComputer science.  
650  0  _aLogic design.  
650  0  _aSoftware engineering.  
650  0  _aComputers.  
650  0  _aComputer logic.  
650  0  _aMathematical logic.  
650  1  4  _aComputer Science. 
650  2  4  _aSoftware Engineering/Programming and Operating Systems. 
650  2  4  _aTheory of Computation. 
650  2  4  _aLogics and Meanings of Programs. 
650  2  4  _aSoftware Engineering. 
650  2  4  _aMathematical Logic and Formal Languages. 
650  2  4  _aLogic Design. 
700  1 
_aHu, Alan J. _eeditor. 

700  1 
_aVardi, Moshe Y. _eeditor. 

710  2  _aSpringerLink (Online service)  
773  0  _tSpringer eBooks  
776  0  8 
_iPrinted edition: _z9783540646082 
830  0 
_aLecture Notes in Computer Science, _x03029743 ; _v1427 

856  4  0  _uhttp://dx.doi.org/10.1007/BFb0028725 
912  _aZDB2SCS  
912  _aZDB2LNC  
912  _aZDB2BAE  
942 
_2ddc _cEB 

950  _aComputer Science (Springer11645)  
999 
_c14560 _d14560 