05776nam a22005295i 4500001001800000003000900018005001700027007001500044008004100059020001800100024002800118050001300146072001600159072001500175072002300190082001400213245019700227264006100424300003200485336002600517337002600543338003600569347002400605490005800629505335400687520060204041650002204643650001804665650002604683650001504709650002004724650002404744650002204768650006004790650002704850650003704877650002604914650004504940650001804985700002505003700002905028710003405057773002005091776003605111830005805147856004105205978-3-540-69339-0DE-He21320170515111459.0cr nn 008mamaa121227s1998 gw | s |||| 0|eng d a97835406933907 a10.1007/BFb00287252doi 4aQA76.758 7aUMZ2bicssc 7aUL2bicssc 7aCOM0512302bisacsh04a005.122310aComputer Aided Verificationh[electronic resource] :b10th International Conference, CAV'98 Vancouver, BC, Canada, June 28 – July 2, 1998 Proceedings /cedited by Alan J. Hu, Moshe Y. Vardi. 1aBerlin, Heidelberg :bSpringer Berlin Heidelberg,c1998. aX, 552 p.bonline resource. atextbtxt2rdacontent acomputerbc2rdamedia aonline resourcebcr2rdacarrier atext filebPDF2rda1 aLecture Notes in Computer Science,x0302-9743 ;v14270 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. 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. 0aComputer science. 0aLogic design. 0aSoftware engineering. 0aComputers. 0aComputer logic. 0aMathematical logic.14aComputer Science.24aSoftware Engineering/Programming and Operating Systems.24aTheory of Computation.24aLogics and Meanings of Programs.24aSoftware Engineering.24aMathematical Logic and Formal Languages.24aLogic Design.1 aHu, Alan J.eeditor.1 aVardi, Moshe Y.eeditor.2 aSpringerLink (Online service)0 tSpringer eBooks08iPrinted edition:z9783540646082 0aLecture Notes in Computer Science,x0302-9743 ;v142740uhttp://dx.doi.org/10.1007/BFb0028725