Formal methods in computer-aided design : 4th international conference, FMCAD 2002, Portland, OR, USA, November 6-8, 2002 : proceedings
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...
Saved in:
| Corporate Author: | |
|---|---|
| Other Authors: | , |
| Format: | Livre numérique |
| Language: | Anglais |
| Published: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Series: | Lecture notes in computer science
2517 |
| Subjects: | |
| Online Access: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Note: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Formal methods in computer-aided design, 4th international conference, FMCAD 2002, Portland, OR, USA, November 6-8, 2002, Proceedings, Mark D. Aagaard, John W. O'Leary (eds.), Berlin, Springer, 2002, 1 vol. (XI-398 p.), Lecture notes in computer science, 3-540-00116-6 • Formal Methods in Computer-Aided Design, Texte imprimé, 9783662198865 |
Table of Contents:
- 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 withRelative Placement Information for Parametrised Libraries
- Prototyping and Synthesis
- Input/Output Compatibility of Reactive Systems
- Smart Play-out of Behavioral Requirements.