Formal Methods in Computer-Aided Design Third International Conference, FMCAD 2000 Austin, TX, USA, November 1-3, 2000 Proceedings /

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

The biannual Formal Methods in Computer Aided Design conference (FMCAD 2000)is the third in a series of conferences under that title devoted to the use of discrete mathematical methods for the analysis of computer hardware and so- ware. The work reported in this book describes the use of modeling la...

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

• Applications of Hierarchical Verification in Model Checking
• Applications of Hierarchical Verification in Model Checking
• Invited Talk
• Trends in Computing
• Invited Paper
• A Case Study in Formal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon TM Processor
• Contributed Papers
• An Algorithm for Strongly Connected Component Analysis in n log n Symbolic Steps
• Automated Refinement Checking for Asynchronous Processes
• Border-Block Triangular Form and Conjunction Schedule in Image Computation
• B2M: A Semantic Based Tool for BLIF Hardware Descriptions
• Checking Safety Properties Using Induction and a SAT-Solver
• Combining Stream-Based and State-Based Verification Techniques
• A Comparative Study of Symbolic Algorithms for the Computation of Fair Cycles
• Correctness of Pipelined Machines
• Do You Trust Your Model Checker?
• Executable Protocol Specification in ESL
• Formal Verification of Floating Point Trigonometric Functions
• Hardware Modeling Using Function Encapsulation
• A Methodology for the Formal Analysis of Asynchronous Micropipelines
• A Methodology for Large-Scale Hardware Verification
• Model Checking Synchronous Timing Diagrams
• Model Reductions and a Case Study
• Modeling and Parameters Synthesis for an Air TrafficManagement System
• Monitor-Based Formal Specification of PCI
• SAT-Based Image Computation with Application in Reachability Analysis
• SAT-Based Verification without State Space Traversal
• Scalable Distributed On-the-Fly Symbolic Model Checking
• The Semantics of Verilog Using Transition System Combinators
• Sequential Equivalence Checking by Symbolic Simulation
• Speeding Up Image Computation by Using RTL Information
• Symbolic Checking of Signal-Transition Consistency for Verifying High-Level Designs
• Symbolic Simulation with Approximate Values
• A Theory of Consistency for Modular Synchronous Systems
• Verifying Transaction Ordering Properties in Unbounded Bus Networks through Combined Deductive/Algorithmic Methods
• Visualizing System Factorizations with Behavior Tables.