Formal Methods in System Design, Volume 14

Volume 14, Number 1, January 1999

Steven M. German: Introduction to the Special Issue on Verification of Arithmetic Hardware. 5-6
Edmund M. Clarke, Steven M. German, Xudong Zhao: Verifying the SRT Division Algorithm Using Theorem Proving Techniques. 7-44
Harald Rueß, Natarajan Shankar, Mandayam K. Srivas: Modular Verification of SRT Division. 45-73
David M. Russinoff: A Mechanically Checked Proof of Correctness of the AMD K5 Floating Point Square Root Microcode. 75-125

Simin Nadjm-Tehrani, Jan-Erik Strömberg: Formal Verification of Dynamic Properties in an Aerospace Application. 135-169
Guy Leduc, Olivier Bonaventure, Luc Léonard, E. Koerner, Charles Pecheur: Model-Based Verification of a Security Protocol for Conditional Access to Services. 171-191
Wai Wong: Validation of HOL Proofs by Proof Checking. 193-212
J. Strother Moore: A Mechanically Checked Proof of a Multiprocessor Result via a Uniprocessor View. 213-228

Rajeev Alur, Thomas A. Henzinger: Introduction. 235
Bernard Boigelot, Patrice Godefroid: Symbolic Verification of Communication Protocols with Infinite State Spaces using QDDs. 237-255
Patrice Godefroid, David E. Long: Symbolic Protocol Verification with Queue BDDs. 257-271
C. Norris Ip, David L. Dill: Verifying Systems with Replicated Components in Mur[b.phiv]. 273-310
Shmuel Katz, Hillel Miller: Saving Space by Fully Exploiting Invisible Transitions. 311-332