7. CHARME 1993: Arles, France

@proceedings{DBLP:conf/charme/1993,
  editor    = {George J. Milne and
               Laurence Pierre},
  title     = {Correct Hardware Design and Verification Methods, IFIP WG 10.5
               Advanced Research Working Conference, CHARME '93, Arles, France,
               May 24-26, 1993, Proceedings},
  booktitle = {CHARME},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {683},
  year      = {1993},
  isbn      = {3-540-56778-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

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