Formal Methods in Computer-Aided Design Second International Conference, FMCAD '98, Palo Alto, CA, USA, November 4-6, 1998, Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Gopalakrishnan, Ganesh (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Windley, Phillip (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1998.
• Έκδοση: 1st ed. 1998.
• Σειρά: Lecture Notes in Computer Science, 1522
• Θέματα: Computer-aided engineering.; Computer hardware.; Computer logic.; Mathematical logic.; Computational complexity.; Computer-Aided Engineering (CAD, CAE) and Design.; Computer Hardware.; Logics and Meanings of Programs.; Mathematical Logic and Formal Languages.; Complexity.

Πίνακας περιεχομένων:

• Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification
• Reducing Manual Abstraction in Formal Verification of Out- of- Order Execution
• Bit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checking
• Solving Bit-Vector Equations
• The Formal Design of 1M-Gate ASICs
• Design of Experiments for Evaluation of BDD Packages Using Controlled Circuit Mutations
• A Tutorial on Stålmarck's Proof Procedure for Propositional Logic
• Almana: A BDD Minimization Tool Integrating Heuristic and RewritingMethods
• Bisimulation Minimization in an Automata-Theoretic Verification Framework
• Automatic Verification of Mixed-Level Logic Circuits
• A Timed Automaton-Based Method for Accurate Computation of Circuit Delay in the Presence of Cross-Talk
• Maximum Time Separation of Events in Cyclic Systems with Linear and Latest Timing Constraints
• Using MTBDDs for Composition and Model Checking of Real-Time Systems
• Formal Methods in CAD from an Industrial Perspective
• A Methodology for Automated Verification of Synthesized RTL Designs and Its Integration with a High-Level Synthesis Tool
• Combined Formal Post- and Presynthesis Verification in High Level Synthesis
• Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem
• A Performance Study of BDD-Based Model Checking
• Symbolic Model Checking Visualization
• Input Elimination and Abstraction in Model Checking
• Symbolic Simulation of the JEM1 Microprocessor
• Symbolic Simulation: An ACL2 Approach
• Verification of Data-Insensitive Circuits: An In-Order-Retirement Case Study
• Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification
• Formally Verifying Data and Control with Weak Reachability Invariants
• Generalized Reversible Rules
• An Assume-Guarantee Rule for Checking Simulation
• Three Approaches to Hardware Verification: HOL, MDG, and VIS Compared
• An Instruction Set Process Calculus
• Techniques for Implicit State Enumeration of EFSMs
• Model Checking on Product Structures
• BDDNOW: A Parallel BDD Package
• Model Checking VHDL with CV
• Alexandria: A Tool for Hierarchical Verification
• PV: An Explicit Enumeration Model-Checker.