Formal Methods in Computer-Aided Design 4th International Conference, FMCAD 2002, Portland, OR, USA, November 6-8, 2002, Proceedings /

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

This volume contains the proceedings of the Fourth Biennial Conference on F- mal Methods in Computer-Aided Design (FMCAD). The conference is devoted to the use of mathematical methods for the analysis of digital hardware c- cuits and systems. The workreported in this bookdescribes the use of formal...

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

• Abstraction
• Abstraction by Symbolic Indexing Transformations
• Counter-Example Based Predicate Discovery in Predicate Abstraction
• Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis
• Symbolic Simulation
• Simplifying Circuits for Formal Verification Using Parametric Representation
• Generalized Symbolic Trajectory Evaluation - Abstraction in Action
• Model Checking: Strongly-Connected Components
• Analysis of Symbolic SCC Hull Algorithms
• Sharp Disjunctive Decomposition for Language Emptiness Checking
• Microprocessor Specification and Verification
• Relating Multi-step and Single-Step Microprocessor Correctness Statements
• Modeling and Verification of Out-of-Order Microprocessors in UCLID
• Decision Procedures
• On Solving Presburger and Linear Arithmetic with SAT
• Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods
• Qubos: Deciding Quantified Boolean Logic Using Propositional Satisfiability Solvers
• Model Checking: Reachability Analysis
• Exploiting Transition Locality in the Disk Based Mur? Verifier
• Traversal Techniques for Concurrent Systems
• Model Checking: Fixed Points
• A Fixpoint Based Encoding for Bounded Model Checking
• Using Edge-Valued Decision Diagrams for Symbolic Generation of Shortest Paths
• Verification Techniques and Methodology
• Mechanical Verification of a Square Root Algorithm Using Taylor's Theorem
• A Specification and Verification Framework for Developing Weak Shared Memory Consistency Protocols
• Model Checking the Design of an Unrestricted, Stuck-at Fault Tolerant, Asynchronous Sequential Circuit Using SMV
• Hardware Description Languages
• Functional Design Using Behavioural and Structural Components
• Compiling Hardware Descriptions with Relative Placement Information for Parametrised Libraries
• Prototyping and Synthesis
• Input/Output Compatibility of Reactive Systems
• Smart Play-out of Behavioral Requirements.