default search action
8. CHARME 1995: Frankfurt/Main, Germany
- Paolo Camurati, Hans Eveking:
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
Model checking
- Hardi Hungar, Orna Grumberg, Werner Damm:
What if model checking must be truly symbolic. 1-20 - Ulrich Stern, David L. Dill:
Automatic verification of the SCI cache coherence protocol. 21-34
Theorem proving
- Laurence Pierre:
Describing and verifying synchronous circuits with the Boyer-Moore theorem prover. 35-55 - Paul Curzon:
Problems encountered in the machine-assisted proof of hardware. 56-70
Formally verified synthesis
- Dirk Eisenbiegler, Ramayya Kumar:
Formally embedding existing high level synthesis algorithms. 71-83 - Li-Guo Wang, Michael Mendler:
Formal design of a class of computers. 84-102
Process algebras
- Michael C. McFarland, Thaddeus J. Kowalski:
Symbolic analysis and verification of CPA descriptions. 103-123 - Ana Cristina Vieira de Melo, Howard Barringer:
A foundation for formal reuse of hardware. 124-145
Finite state systems 1
- Francisco Corella, Michel Langevin, Eduard Cerny, Zijian Zhou, Xiaoyu Song:
State enumeration with abstract descriptions of state machines. 146-160 - Gianpiero Cabodi, Stefano Quer, Paolo Camurati:
Transforming boolean relations by symbolic encoding. 161-170 - Ayman M. Wahba, Dominique Borrione:
Design error diagnosis in sequential circuits. 171-188
Finite state systems 2
- Oded Maler, Amir Pnueli:
Timing analysis of asynchronous circuits using timed automata. 189-205 - Ulrich Stern, David L. Dill:
Improved probabilistic verification by hash compaction. 206-224
Verification environments
- Howard Barringer, Graham Gough, Brian Monahan, Alan R. Williams:
Formal support for the ELLA hardwar description language. 225-245 - Rocco De Nicola, Alessandro Fantechi, Stefania Gnesi, Salvatore Larosa, Gioia Ristori:
Verifying hardware components within JACK. 246-260
Language containment
- Serdar Tasiran, Ramin Hojati, Robert K. Brayton:
Language containment of non-deterministic omega-automata. 261-277 - Dominique Bolignano:
A partial-order approach to the verification of concurrent systems: checking liveness properties. 278-292
VHDL
- David Déharbe, Dominique Borrione:
Semantics of a verification-oriented subset of VHDL. 293-310 - Kees G. W. Goossens:
Reasoning about VHDL using operational and observational semantics. 311-327 - Emmanuelle Encrenaz:
A Symbolic Relation for a Subset of VHDL'87 Descriptions and its Application to Symbolic Model Checking. 328-342
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.