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 BibTeX

@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 BibTeX
Serafín Olcoz, José Manuel Colom: A Petri Net Approach for the Analysis of VHDL Descriptions. 15-26 BibTeX
Alan R. Martello, Steven P. Levitan: Temporal Analysis of Time Bounded Digital Systems. 27-38 BibTeX
Keith Hanna, Neil Daeche: Strongly-Typed Theory of Structures and Behaviours. 39-54 BibTeX

2. Verification and Diagnosis

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

3. Proof of Microprocessors

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

4. Temporal and Behavioural Verification II

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

5. Asynchronous Circuit Design

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

6. Hardware Derivation

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

7. Use of Theorem Provers

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