LEADER 06987nam 22007335 450 001 996465394203316 005 20200704184029.0 010 $a3-540-69195-2 024 7 $a10.1007/3-540-63166-6 035 $a(CKB)1000000000234662 035 $a(SSID)ssj0000322082 035 $a(PQKBManifestationID)11282752 035 $a(PQKBTitleCode)TC0000322082 035 $a(PQKBWorkID)10282616 035 $a(PQKB)10418328 035 $a(DE-He213)978-3-540-69195-2 035 $a(PPN)155226746 035 $a(EXLCZ)991000000000234662 100 $a20121227d1997 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aComputer Aided Verification$b[electronic resource] $e9th International Conference, CAV'97, Haifa, Israel, June 22-25, 1997, Proceedings /$fedited by Orna Grumberg 205 $a1st ed. 1997. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1997. 215 $a1 online resource (XII, 492 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v1254 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-63166-6 327 $aPractical challenges for industrial formal verification tools -- Formal verification of digital systems, from ASICs to HW/SW codesign ? a pragmatic approach -- The industrial success of verification tools based on stålmarck's method -- Formal verification ? Applications & case studies -- Automatic abstraction techniques for propositional ?-calculus model checking -- A compositional rule for hardware design refinement -- Module checking revisited -- Using compositional preorders in the verification of sliding window protocol -- An efficient decision procedure for the theory of fixed-sized bit-vectors -- Construction of abstract state graphs with PVS -- Verification of a chemical process leak test procedure -- Automatic datapath extraction for efficient usage of HDD -- An n log n algorithm for online BDD refinement -- Weak bisimulation for fully probabilistic processes -- Towards a mechanization of cryptographic protocol verification -- Efficient model checking using tabled resolution -- Containment of regular languages in non-regular timing diagram languages is decidable -- An improved reachability analysis method for strongly linear hybrid systems (extended abstract) -- Some progress in the symbolic verification of timed automata -- STARI: A case study in compositional and hierarchical timing verification -- A provably correct embedded verifier for the certification of safety critical software -- Model checking in a microprocessor design project -- Some thoughts on statecharts, 13 years later -- On-the-fly model checking under fairness that exploits symmetry -- Exploiting symmetry when verifying transistor-level circuits by symbolic trajectory evaluation -- Parallelizing the Mur? verifier -- A new heuristic for bad cycle detection using BDDs -- Efficient detection of vacuity in ACTL formulas -- Model checking and transitive-closure logic -- Boolean and 2-adic numbers based techniques for verifying synchronous designs -- Programs with quasi-stable channels are effectively recognizable -- Combining constraint solving and symbolic model checking for a class of systems with non-linear constraints -- Relaxed visibility enhances partial order reduction -- Partial-order reduction in symbolic state space exploration -- Deadlock checking using net unfoldings -- Trace table based approach for pipelined microprocessor verification -- On combining formal and informal verification -- Efficient modeling of memory arrays in symbolic simulation -- Symbolic model checking of infinite state systems using presburger arithmetic -- Parametrized verification of linear networks using automata as invariants -- Symbolic model checking with rich assertional languages -- The invariant checker: Automated deductive verification of reactive systems -- The PEP tool -- TermiLog: A system for checking termination of queries to logic programs -- Mosel: A sound and efficient tool for M2L(Str) -- The verus tool: A quantitative approach to the formal verification of real-time systems -- Uppaal: Status & developments -- HyTech: A model checker for hybrid systems -- SMC: A symmetry based model checker for verification of liveness properties -- ?cke ? Efficient ?-calculus model checking -- Prod 3.2 An advanced tool for efficient reachability analysis -- VeriSoft: A tool for the automatic analysis of concurrent reactive software -- RuleBase: Model checking at IBM. 330 $aThis book constitutes the strictly refereed proceedings of the 9th International Conference on Computer Aided Verification, CAV '97, held in Haifa, Israel, in June 1997. The volume presents 34 revised full papers selected from a total of 84 submissions. Also included are 7 invited contributions as well as 12 tool descriptions. The volume is dedicated to the theory and practice of computer aided formal methods for software and hardware verification, with an emphasis on verification tools and algorithms and the techniques needed for their implementation. The book is a unique record documenting the recent progress in the area. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v1254 606 $aComputers 606 $aComputer logic 606 $aSoftware engineering 606 $aMathematical logic 606 $aSpecial purpose computers 606 $aArtificial intelligence 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 $aSpecial Purpose and Application-Based Systems$3https://scigraph.springernature.com/ontologies/product-market-codes/I13030 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 615 0$aComputers. 615 0$aComputer logic. 615 0$aSoftware engineering. 615 0$aMathematical logic. 615 0$aSpecial purpose computers. 615 0$aArtificial intelligence. 615 14$aTheory of Computation. 615 24$aLogics and Meanings of Programs. 615 24$aSoftware Engineering. 615 24$aMathematical Logic and Formal Languages. 615 24$aSpecial Purpose and Application-Based Systems. 615 24$aArtificial Intelligence. 676 $a004.0151 702 $aGrumberg$b Orna$4edt$4http://id.loc.gov/vocabulary/relators/edt 906 $aBOOK 912 $a996465394203316 996 $aComputer Aided Verification$9772228 997 $aUNISA