8. CHARME 1995: Frankfurt/Main, Germany

Paolo Camurati, Hans Eveking (Eds.): Correct Hardware Design and Verification Methods, IFIP WG 10.5 Advanced Research Working Conference, CHARME '95, Frankfurt/Main, Germany, October 2-4, 1995, Proceedings. Lecture Notes in Computer Science 987 Springer 1995, ISBN 3-540-60385-9 BibTeX

@proceedings{DBLP:conf/charme/1995,
  editor    = {Paolo Camurati and
               Hans Eveking},
  title     = {Correct Hardware Design and Verification Methods, IFIP WG 10.5
               Advanced Research Working Conference, CHARME '95, Frankfurt/Main,
               Germany, October 2-4, 1995, Proceedings},
  booktitle = {CHARME},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {987},
  year      = {1995},
  isbn      = {3-540-60385-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Model checking

Hardi Hungar, Orna Grumberg, Werner Damm: What if model checking must be truly symbolic. 1-20 BibTeX
Ulrich Stern, David L. Dill: Automatic verification of the SCI cache coherence protocol. 21-34 BibTeX

Theorem proving

Laurence Pierre: Describing and verifying synchronous circuits with the Boyer-Moore theorem prover. 35-55 BibTeX
Paul Curzon: Problems encountered in the machine-assisted proof of hardware. 56-70 BibTeX

Formally verified synthesis

Dirk Eisenbiegler, Ramayya Kumar: Formally embedding existing high level synthesis algorithms. 71-83 BibTeX
Li-Guo Wang, Michael Mendler: Formal design of a class of computers. 84-102 BibTeX

Process algebras

Michael C. McFarland, Thaddeus J. Kowalski: Symbolic analysis and verification of CPA descriptions. 103-123 BibTeX
Ana Cristina Vieira de Melo, Howard Barringer: A foundation for formal reuse of hardware. 124-145 BibTeX

Finite state systems 1

Francisco Corella, Michel Langevin, Eduard Cerny, Zijian Zhou, Xiaoyu Song: State enumeration with abstract descriptions of state machines. 146-160 BibTeX
Gianpiero Cabodi, Stefano Quer, Paolo Camurati: Transforming boolean relations by symbolic encoding. 161-170 BibTeX
Ayman M. Wahba, Dominique Borrione: Design error diagnosis in sequential circuits. 171-188 BibTeX

Finite state systems 2

Oded Maler, Amir Pnueli: Timing analysis of asynchronous circuits using timed automata. 189-205 BibTeX
Ulrich Stern, David L. Dill: Improved probabilistic verification by hash compaction. 206-224 BibTeX

Verification environments

Howard Barringer, Graham Gough, Brian Monahan, Alan Williams: Formal support for the ELLA hardwar description language. 225-245 BibTeX
Rocco De Nicola, Alessandro Fantechi, Stefania Gnesi, Salvatore Larosa, Gioia Ristori: Verifying hardware components within JACK. 246-260 BibTeX

Language containment

Serdar Tasiran, Ramin Hojati, Robert K. Brayton: Language containment of non-deterministic omega-automata. 261-277 BibTeX
Dominique Bolignano: A partial-order approach to the verification of concurrent systems: checking liveness properties. 278-292 BibTeX

VHDL

David Déharbe, Dominique Borrione: Semantics of a verification-oriented subset of VHDL. 293-310 BibTeX
Kees G. W. Goossens: Reasoning about VHDL using operational and observational semantics. 311-327 BibTeX
Emmanuelle Encrenaz: A Symbolic Relation for a Subset of VHDL'87 Descriptions and its Application to Symbolic Model Checking. 328-342 BibTeX