LEADER 06919nam 22007215 450 001 9910144909603321 005 20200630135826.0 010 $a3-540-69339-4 024 7 $a10.1007/BFb0028725 035 $a(CKB)1000000000234810 035 $a(SSID)ssj0000322083 035 $a(PQKBManifestationID)11282753 035 $a(PQKBTitleCode)TC0000322083 035 $a(PQKBWorkID)10281159 035 $a(PQKB)10296549 035 $a(DE-He213)978-3-540-69339-0 035 $a(PPN)155216201 035 $a(EXLCZ)991000000000234810 100 $a20121227d1998 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aComputer Aided Verification$b[electronic resource] $e10th International Conference, CAV'98, Vancouver, BC, Canada, June 28-July 2, 1998, Proceedings /$fedited by Alan J. Hu, Moshe Y. Vardi 205 $a1st ed. 1998. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1998. 215 $a1 online resource (X, 552 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v1427 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-64608-6 327 $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 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. 330 $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 state-space exploration, model checking, synthesis, and automated deduction; various verification techniques; applications and case studies, and verification in practice. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v1427 606 $aSoftware engineering 606 $aComputers 606 $aComputer logic 606 $aLogic, Symbolic and mathematical 606 $aLogic design 606 $aSoftware Engineering/Programming and Operating Systems$3https://scigraph.springernature.com/ontologies/product-market-codes/I14002 606 $aTheory of Computation$3https://scigraph.springernature.com/ontologies/product-market-codes/I16005 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aLogic Design$3https://scigraph.springernature.com/ontologies/product-market-codes/I12050 615 0$aSoftware engineering. 615 0$aComputers. 615 0$aComputer logic. 615 0$aLogic, Symbolic and mathematical. 615 0$aLogic design. 615 14$aSoftware Engineering/Programming and Operating Systems. 615 24$aTheory of Computation. 615 24$aLogics and Meanings of Programs. 615 24$aSoftware Engineering. 615 24$aMathematical Logic and Formal Languages. 615 24$aLogic Design. 676 $a005.1 702 $aHu$b Alan J$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aVardi$b Moshe Y$4edt$4http://id.loc.gov/vocabulary/relators/edt 906 $aBOOK 912 $a9910144909603321 996 $aComputer Aided Verification$93027789 997 $aUNINA