LEADER 05002nam 22007335 450 001 996466103703316 005 20200702132921.0 010 $a3-540-45516-7 024 7 $a10.1007/3-540-60385-9 035 $a(CKB)1000000000234351 035 $a(SSID)ssj0000322363 035 $a(PQKBManifestationID)11213943 035 $a(PQKBTitleCode)TC0000322363 035 $a(PQKBWorkID)10286910 035 $a(PQKB)10600703 035 $a(DE-He213)978-3-540-45516-5 035 $a(PPN)155179284 035 $a(EXLCZ)991000000000234351 100 $a20121227d1995 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aCorrect Hardware Design and Verification Methods$b[electronic resource] $eIFIP WG10.5 Advanced Research Working Conference, CHARME '95, Frankfurt, Germany, October 1995. Proceedings /$fedited by Paolo Enrico Camurati, Hans Eveking 205 $a1st ed. 1995. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1995. 215 $a1 online resource (X, 346 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v987 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-60385-9 327 $aWhat if model checking must be truly symbolic -- Automatic verification of the SCI cache coherence protocol -- Describing and verifying synchronous circuits with the Boyer-Moore theorem prover -- Problems encountered in the machine-assisted proof of hardware -- Formally embedding existing high level synthesis algorithms -- Formal design of a class of computers ? its high stage: abstract microprogramming -- Symbolic analysis and verification of CPA descriptions -- A foundation for formal reuse of hardware -- State enumeration with abstract descriptions of state machines -- Transforming Boolean relations by symbolic encoding -- Design error diagnosis in sequential circuits -- Timing analysis of asynchronous circuits using timed automata -- Improved probabilistic verification by hash compaction -- Formal support for the ELLA hardware description language -- Verifying hardware components with JACK -- Language containment of non-deterministic ?-automata -- A partial-order approach to the verification of concurrent systems: Checking liveness properties -- Semantics of a verification-oriented subset of VHDL -- Reasoning about VHDL using operational and observational semantics -- A symbolic relation for a subset of VHDL'87 descriptions and its application to symbolic model checking. 330 $aThis book constitutes the refereed proceedings of the IFIP WG10.5 Advanced Research Working Conference on Correct Hardware Design Methodologies, CHARME '95, held in Frankfurt, Germany, in October 1995. The 20 revised full papers presented were carefully selected by the program committee and address all current aspects of research and advanced applications in the field of formal verification of hardware. Among the topics covered are model checking, theorem proving, formally verified synthesis, process algebras, finite state systems, verification environments, language containment, and VHDL. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v987 606 $aArchitecture, Computer 606 $aElectronics 606 $aMicroelectronics 606 $aInput-output equipment (Computers) 606 $aSoftware engineering 606 $aComputer logic 606 $aComputer System Implementation$3https://scigraph.springernature.com/ontologies/product-market-codes/I13057 606 $aElectronics and Microelectronics, Instrumentation$3https://scigraph.springernature.com/ontologies/product-market-codes/T24027 606 $aInput/Output and Data Communications$3https://scigraph.springernature.com/ontologies/product-market-codes/I12042 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 615 0$aArchitecture, Computer. 615 0$aElectronics. 615 0$aMicroelectronics. 615 0$aInput-output equipment (Computers). 615 0$aSoftware engineering. 615 0$aComputer logic. 615 14$aComputer System Implementation. 615 24$aElectronics and Microelectronics, Instrumentation. 615 24$aInput/Output and Data Communications. 615 24$aSoftware Engineering. 615 24$aLogics and Meanings of Programs. 676 $a621.39/5 702 $aCamurati$b Paolo Enrico$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aEveking$b Hans$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aAdvanced Research Working Conference on Correct Hardware Design Methodologies 906 $aBOOK 912 $a996466103703316 996 $aCorrect Hardware Design and Verification Methods$9772373 997 $aUNISA