LEADER 06945nam 22008055 450 001 9910144338003321 005 20200630070712.0 010 $a3-540-30494-0 024 7 $a10.1007/b102264 035 $a(CKB)1000000000212624 035 $a(DE-He213)978-3-540-30494-4 035 $a(SSID)ssj0000157235 035 $a(PQKBManifestationID)11151059 035 $a(PQKBTitleCode)TC0000157235 035 $a(PQKBWorkID)10131303 035 $a(PQKB)11592723 035 $a(MiAaPQ)EBC3087703 035 $a(PPN)155195050 035 $a(EXLCZ)991000000000212624 100 $a20121227d2004 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aFormal Methods in Computer-Aided Design $e5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings /$fedited by Alan J. Hu, Andrew K. Martin 205 $a1st ed. 2004. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2004. 215 $a1 online resource (XII, 448 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v3312 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-23738-0 320 $aIncludes bibliographical references at the end of each chapters and index. 327 $aChallenges in System-Level Design -- Generating Fast Multipliers Using Clever Circuits -- Verification of Analog and Mixed-Signal Circuits Using Hybrid System Techniques -- A Methodology for the Formal Verification of FFT Algorithms in HOL -- A Functional Approach to the Formal Specification of Networks on Chip -- Proof Styles in Operational Semantics -- Integrating Reasoning About Ordinal Arithmetic into ACL2 -- Combining Equivalence Verification and Completion Functions -- Synchronization-at-Retirement for Pipeline Verification -- Late Design Changes (ECOs) for Sequentially Optimized Esterel Designs -- Non-miter-based Combinational Equivalence Checking by Comparing BDDs with Different Variable Orders -- Scalable Automated Verification via Expert-System Guided Transformations -- Simple Yet Efficient Improvements of SAT Based Bounded Model Checking -- Simple Bounded LTL Model Checking -- QuBE++: An Efficient QBF Solver -- Bounded Probabilistic Model Checking with the Mur? Verifier -- Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States -- Bounded Verification of Past LTL -- A Hybrid of Counterexample-Based and Proof-Based Abstraction -- Memory Efficient All-Solutions SAT Solver and Its Application for Reachability Analysis -- Approximate Symbolic Model Checking for Incomplete Designs -- Extending Extended Vacuity -- Parameterized Vacuity -- An Operational Semantics for Weak PSL -- Accepting Predecessors Are Better than Back Edges in Distributed LTL Model-Checking -- Bloom Filters in Probabilistic Verification -- A Simple Method for Parameterized Verification of Cache Coherence Protocols -- A Partitioning Methodology for BDD-Based Verification -- Invariant Checking Combining Forward and Backward Traversal -- Variable Reuse for Efficient Image Computation. 330 $aThese are the proceedings of the fifth international conference, Formal Methods in Computer-Aided Design (FMCAD), held 15?17 November 2004 in Austin, Texas, USA. The conference provides a forum for presenting state-of-the-art tools, methods, algorithms, and theory for the application of formalized reasoning to all aspects of computer-aided system design, including specification, verification, synthesis, and testing. FMCAD?s heritage dates back 20 years to some of the earliest conferences on the subject of formal reasoning and computer-aided design. Since 1996,FMCAD has assumed its present form, held biennially in North America, alternating with its sister conference CHARME in Europe. We are delighted to report that our research community continues to flourish: we received 69 paper submissions,with many more high-quality papers than we had room to accept. After a rigorous review process, in which each paper received at least three, and typically four or more, independent reviews, we accepted 29 papers for the conference and inclusion in this volume. The conference also included invited talks from Greg Spirakis of Intel Corporation and Wayne Wolf of Princeton University. A conference of this size requires the contributions of numerous people. On the technical side, we are grateful to the program committee and the additional reviewers for their countless hours reviewing submissions and ensuring the intellectual quality of the conference. We would also like to thank the steering committee for their wisdom and guidance. On the logistical side, we thank Christa Mace for designing our website and attending to countless organizational tasks. And we thank our corporate sponsors ? AMD, IBM, Intel, and Synopsys ? for financial support that helped make this conference possible. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v3312 606 $aComputer-aided engineering 606 $aComputer hardware 606 $aSoftware engineering 606 $aComputer logic 606 $aMathematical logic 606 $aArtificial intelligence 606 $aComputer-Aided Engineering (CAD, CAE) and Design$3https://scigraph.springernature.com/ontologies/product-market-codes/I23044 606 $aComputer Hardware$3https://scigraph.springernature.com/ontologies/product-market-codes/I1200X 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 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 615 0$aComputer-aided engineering. 615 0$aComputer hardware. 615 0$aSoftware engineering. 615 0$aComputer logic. 615 0$aMathematical logic. 615 0$aArtificial intelligence. 615 14$aComputer-Aided Engineering (CAD, CAE) and Design. 615 24$aComputer Hardware. 615 24$aSoftware Engineering. 615 24$aLogics and Meanings of Programs. 615 24$aMathematical Logic and Formal Languages. 615 24$aArtificial Intelligence. 676 $a621.39/5 702 $aHu$b Alan J$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aMartin$b Andrew K$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910144338003321 996 $aFormal Methods in Computer-Aided Design$91891319 997 $aUNINA