LEADER 05861nam 22007455 450 001 996465860903316 005 20230406032333.0 024 7 $a10.1007/11560548 035 $a(CKB)1000000000213281 035 $a(SSID)ssj0000317038 035 $a(PQKBManifestationID)11240581 035 $a(PQKBTitleCode)TC0000317038 035 $a(PQKBWorkID)10295905 035 $a(PQKB)10067688 035 $a(DE-He213)978-3-540-32030-2 035 $a(MiAaPQ)EBC3067864 035 $a(PPN)123097800 035 $a(EXLCZ)991000000000213281 100 $a20100319d2005 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] $e13th IFIP WG 10.5Advanced Research, Working Conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005, Proceedings /$fedited by Dominique Borrione, Wolfgang Paul 205 $a1st ed. 2005. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2005. 215 $a1 online resource (XII, 414 p.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v3725 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-32030-X 311 $a3-540-29105-9 320 $aIncludes bibliographical references and index. 327 $aInvited Talks -- Is Formal Verification Bound to Remain a Junior Partner of Simulation? -- Verification Challenges in Configurable Processor Design with ASIP Meister -- Tutorial -- Towards the Pervasive Verification of Automotive Systems -- Functional Approaches to Design Description -- Wired: Wire-Aware Circuit Design -- Formalization of the DE2 Language -- Game Solving Approaches -- Finding and Fixing Faults -- Verifying Quantitative Properties Using Bound Functions -- Abstraction -- How Thorough Is Thorough Enough? -- Interleaved Invariant Checking with Dynamic Abstraction -- Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units -- Algorithms and Techniques for Speeding (DD-Based) Verification 1 -- Efficient Symbolic Simulation via Dynamic Scheduling, Don?t Caring, and Case Splitting -- Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation -- Saturation-Based Symbolic Reachability Analysis Using Conjunctive and Disjunctive Partitioning -- Real Time and LTL Model Checking -- Real-Time Model Checking Is Really Simple -- Temporal Modalities for Concisely Capturing Timing Diagrams -- Regular Vacuity -- Algorithms and Techniques for Speeding Verification 2 -- Automatic Generation of Hints for Symbolic Traversal -- Maximal Input Reduction of Sequential Netlists via Synergistic Reparameterization and Localization Strategies -- A New SAT-Based Algorithm for Symbolic Trajectory Evaluation -- Evaluation of SAT-Based Tools -- An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment -- Model Reduction -- Exploiting Constraints in Transformation-Based Verification -- Identification and Counter Abstraction for Full Virtual Symmetry -- Verification of Memory Hierarchy Mechanisms -- On the Verification of Memory Management Mechanisms -- Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification -- Short Papers -- Symbolic Partial Order Reduction for Rule Based Transition Systems -- Verifying Timing Behavior by Abstract Interpretation of Executable Code -- Behavior-RTL Equivalence Checking Based on Data Transfer Analysis with Virtual Controllers and Datapaths -- Deadlock Prevention in the Æthereal Protocol -- Acceleration of SAT-Based Iterative Property Checking -- Error Detection Using BMC in a Parallel Environment -- Formal Verification of Synchronizers -- A Parameterized Benchmark Suite of Hard Pipelined-Machine-Verification Problems -- Improvements to the Implementation of Interpolant-Based Model Checking -- High-Level Modelling, Analysis, and Verification on FPGA-Based Hardware Design -- Proving Parameterized Systems: The Use of Pseudo-Pipelines in Polyhedral Logic -- Resolving Quartz Overloading -- FPGA Based Accelerator for 3-SAT Conflict Analysis in SAT Solvers -- Predictive Reachability Using a Sample-Based Approach -- Minimizing Counterexample of ACTL Property -- Data Refinement for Synchronous System Specification and Construction -- Introducing Abstractions via Rewriting -- A Case Study: Formal Verification of Processor Critical Properties. 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v3725 606 $aComputer science 606 $aComputers 606 $aSoftware engineering 606 $aMachine theory 606 $aArtificial intelligence 606 $aTheory of Computation 606 $aComputer Hardware 606 $aComputer Science Logic and Foundations of Programming 606 $aSoftware Engineering 606 $aFormal Languages and Automata Theory 606 $aArtificial Intelligence 615 0$aComputer science. 615 0$aComputers. 615 0$aSoftware engineering. 615 0$aMachine theory. 615 0$aArtificial intelligence. 615 14$aTheory of Computation. 615 24$aComputer Hardware. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aSoftware Engineering. 615 24$aFormal Languages and Automata Theory. 615 24$aArtificial Intelligence. 676 $a621.39/5 702 $aBorrione$b Dominique$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aPaul$b Wolfgang$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 02$aIFIP WG 10.5. 906 $aBOOK 912 $a996465860903316 996 $aCorrect Hardware Design and Verification Methods$9772373 997 $aUNISA