Volume 4, Number 1, 2002

• 
  Mary Shaw: What makes good research in software engineering? 1-7

Special Section on Spin

• 
  Klaus Havelund, Willem Visser: Program model checking as a new trend. 8-20
• 
  Ed Brinksma, Angelika Mader, Ansgar Fehnker: Verification and optimization of a PLC control schedule. 21-33
• 
  James C. Corbett, Matthew B. Dwyer, John Hatcliff, Robby: Expressing checkable properties of dynamic systems: the Bandera Specification Language. 34-56
• 
  Heikki Tauriainen, Keijo Heljanko: Testing LTL formula translation into Büchi automata. 57-70
• 
  Scott D. Stoller: Model-checking multi-threaded distributed Java programs. 71-91
• 
  Dragan Bosnacki, Dennis Dams, Leszek Holenderski: Symmetric Spin. 92-106

Regular Contributions

• 
  Cindy Eisner: Using symbolic CTL model checking to verify the railway stations of Hoorn-Kersenboogerd and Heerhugowaard. 107-124
• 
  Edmund M. Clarke, Masahiro Fujita, Sreeranga P. Rajan, Thomas W. Reps, Subash Shankar, Tim Teitelbaum: Program slicing for VHDL. 125-137

Volume 4, Number 2, February 2003

• 
  Susanne Graf: Preface by the section editor. 139-141
• 
  Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu: Using static analysis to improve automatic test generation. 142-152
• 
  Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, Markus Siegle: A tool for model-checking Markov chains. 153-172
• 
  Edmund M. Clarke, Somesh Jha, Wilfredo R. Marrero: Efficient verification of security protocols using partial-order reductions. 173-188
• 
  Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Thomas F. Melham: The PROSPER toolkit. 189-210
• 
  Steven D. Johnson, Yanhong A. Liu, Yuchen Zhang: A systematic incrementalization technique and its application to hardware design. 211-223
• 
  Orna Kupferman, Moshe Y. Vardi: Vacuity detection in temporal model checking. 224-233
• 
  Hong Peng, Sofiène Tahar, Ferhat Khendek: Comparison of SPIN and VIS for protocol verification. 234-245
• 
  Theo C. Ruys, Ed Brinksma: Managing the verification trajectory. 246-259

Volume 4, Number 3, May 2003

• 
  Jeannette M. Wing: Platitudes and attitudes. 261-265
• 
  Tiziana Margaria: Preface by the section editor. 266-270
• 
  Alan Mycroft, Richard Sharp: Higher-level techniques for hardware description and synthesis. 271-297
• 
  Mark Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones: A framework for superscalar microprocessor correctness statements. 298-312
• 
  Skander Kort, Sofiène Tahar, Paul Curzon: Hierarchical formal verification using a hybrid tool. 313-322
• 
  Roope Kaivola, Katherine R. Kohatsu: Proof engineering in the large: formal verification of Pentium?4 floating-point divider. 323-334
• 
  Fady Copty, Amitai Irron, Osnat Weissberg, Nathan P. Kropp, Gila Kamhi: Efficient debugging in a formal verification environment. 335-348
• 
  Koen Claessen, Mary Sheeran, Satnam Singh: Using Lava to design and verify recursive and periodic sorters. 349-358
• 
  Xiaohua Kong, Radu Negulescu, Larry Weidong Ying: Refinement-based formal verification with heterogeneous timing. 359-370
• 
  César A. Muñoz, Victor Carreño, Gilles Dowek, Ricky W. Butler: Formal verification of conflict detection algorithms. 371-380
• 
  Karim El Guemhioui: A framework for distributing object-oriented designs. 381-396

Volume 4, Number 4, August 2003

The Opinion Corner

• 
  Dieter Hogrefe: Main issues in protocol testing. 397-400

Special section: An experience in the establishment of collaboration between academia and industry

• 
  Bengt Jonsson, Konstantinos F. Sagonas: Preface by the section editors. 401-404
• 
  Lars-Åke Fredlund, Dilian Gurov, Thomas Noll, Mads Dam, Thomas Arts, Gennady Chugunov: A verification tool for ERLANG. 405-420
• 
  Erik Johansson, Mikael Pettersson, Konstantinos F. Sagonas, Thomas Lindgren: The development of the HiPE system: design and experience report. 421-436
• 
  Jakob Engblom, Andreas Ermedahl, Mikael Sjödin, Jan Gustafsson, Hans Hansson: Worst-case execution-time analysis for embedded real-time systems. 437-455
• 
  John Håkansson, Bengt Jonsson, Ola Lundqvist: Generating online test oracles from temporal logic specifications. 456-471

Regular Contributions

• 
  Mourad Debbabi, Nancy A. Durgin, Mohamed Mejri, John C. Mitchell: Security by typing. 472-495
• 
  Shoham Ben-David, Orna Grumberg, Tamir Heyman, Assaf Schuster: Scalable distributed on-the-fly symbolic model checking. 496-504
• 
  Yifei Dong, Xiaoqun Du, Gerard J. Holzmann, Scott A. Smolka: Fighting livelock in the GNU i-protocol: a case study in explicit-state model checking. 505-528