7. CHARME 1993: Arles, France

George J. Milne, Laurence Pierre (Eds.): Correct Hardware Design and Verification Methods, IFIP WG 10.5 Advanced Research Working Conference, CHARME '93, Arles, France, May 24-26, 1993, Proceedings. Lecture Notes in Computer Science 683 Springer 1993, ISBN 3-540-56778-X

1. Temporal and Behavioural Verification I

Viktor Cingel:
A Graph-Based Method for Timing Diagrams Representation and Verification. 1-14
Serafín Olcoz, José Manuel Colom:
A Petri Net Approach for the Analysis of VHDL Descriptions. 15-26
Alan R. Martello, Steven P. Levitan:
Temporal Analysis of Time Bounded Digital Systems. 27-38
Keith Hanna, Neil Daeche:
Strongly-Typed Theory of Structures and Behaviours. 39-54

2. Verification and Diagnosis

Ayman M. Wahba, Einar J. Aas:
Verification and Diagnosis of Digital Systems by Termary Reasoning. 55-67
Qinhai Zhang, Charles Trullemans:
Logic Verification of Incomplete Functions and Design Error Location. 68-79
Paolo Camurati, Fulvio Corno, Paolo Prinetto:
A Methodology for System-Level Design for Verifiability. 80-91

3. Proof of Microprocessors

Neal A. Harman, J. V. Tucker:
Algebraic Models and the Correctness of Microprocessors. 92-108
Jacques Chazarain, Hélène Collavizza:
Combining Symbolic Evaluation and Object-Oriented Approach for Verifying Processor-Like Architectures at the RT-Level. 109-121
Phillip J. Windley:
A Theory of Generic Interpreters. 122-134

4. Temporal and Behavioural Verification II

P. A. Subrahmanyam:
Towards Verifying Large(r) Systems: A Strategy and an Experiment. 135-154
Gianpiero Cabodi, Paolo Camurati:
Advancements in Symbolic Traversal Technique. 155-166

5. Asynchronous Circuit Design

Andrew M. Bailey:
Automatic Verification of Speed-Independent Circuit Designs Using the Circal System. 167-178
Scott F. Smith, Amy E. Zwarico:
Correct Compilation of Specifications to Deterministic Asynchronous Circuits. 179-190

6. Hardware Derivation

Bhaskar Bose, Steven D. Johnson:
DDD-FM9001: Derivation of a Verified Microprocessor. 191-202
Joep L. W. Kessels:
Calculational Derivation of a Counter with Bounded Response Time. 203-213
Jifeng He, Ian Page, Jonathan P. Bowen:
Towards a Provably Correct Hardware Implementation of Occam. 214-225
Robin Sharp, Ole Rasmussen:
Rewriting with Constraints in T-Ruby. 226-241

7. Use of Theorem Provers

Thomas Kropf, Ramayya Kumar, Klaus Schneider:
Embedding Hardware Verification Within a Commercial Design Framework. 242-257
Per Bojsen:
An Approach to Formalization of Data Flow Graphs. 258-269

Last update Sun May 26 01:32:27 2013 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page