Volume 2, Number 1, 1998

The Opinion Corner

• 
  Gregor Snelting: Paul Feyerabend and Software Technology. 1-5

Special Section on Program Analysis Tools

• 
  Chris Hankin: Program Analysis Tools. 6-12
• 
  Torben Amtoft, Hanne Riis Nielson, Flemming Nielson: Behavior Analysis for Validating Communication Patterns. 13-28
• 
  Michael Codish, Bart Demoen, Konstantinos F. Sagonas: Semantics-Based Program Analysis for Logic-Based Languages Using XSB. 29-45
• 
  Florian Martin: PAG - An Efficient Program Analyzer Generator. 46-67

Regular Contribution

• 
  Mihaela Sighireanu, Radu Mateescu: Verification of the Link Layer Protocol of the IEEE-1394 Serial Bus (FireWire): An Experiment with E-LOTOS. 68-88

Volume 2, Number 2, 1998

The Opinion Corner

• 
  Perdita Stevens: A Verification Tool Seveloper's Vade Mecum. 89-94

Special Section on Coloured Petri Nets

• 
  Kurt Jensen: Coloured Petri Nets - Preface by the Section Editor. 95-97
• 
  Lars Michael Kristensen, Søren Christensen, Kurt Jensen: The Practitioner's Guide to Coloured Petri Nets. 98-132
• 
  Jianli Xu, Juha Kuusela: Analyzing the Execution Architecture of Mobile Phone Software with Colored Petri Nets. 133-143
• 
  Steven Gordon, Jonathan Billington: Analysing a Missile Simulator with Coloured Petri Nets. 144-159
• 
  Gilles Moncelet, Søren Christensen, Hamid Demmou, Mario Paludetto, José Porras: Analysing a Mechatronic System with Coloured Petri Nets. 160-167
• 
  Lee W. Wagenhals, Insub Shin, Alexander H. Levis: Creating Executable Models of Influence Nets with Colored Petri Nets. 168-181
• 
  Frank P. Burns, Albert Koelmans, Alexandre Yakovlev: Analysing Superscalar Processor Architectures with Coloured Petri Nets. 182-191

Regular Contribution

• 
  Amir Pnueli, Ofer Strichman, Michael Siegel: The Code Validation Tool CVT: Automatic Verification of a Compilation Process. 192-201

Technical Innovation

• 
  Thomas Friese, Tiziana Margaria, Alfred Hofmann: Integrating Printed and Online Information. 202

Volume 2, Number 3, 1999

The Opinion Corner

• 
  Steven D. Johnson: A Workshop on Formal Methods Education: An Aggregation of Opinions. 203-207

Special Section on Model Checking

• 
  Rance Cleaveland: Pragmatics of Model Checking: An STTT Special Section. 208-218
• 
  Xiaoqun Du, Scott A. Smolka, Rance Cleaveland: Local Model Checking and Protocol Analysis. 219-241
• 
  Henrik Reif Andersen, Jørn Lind-Nielsen: Partial Model Checking of Modal Equations: A Survey. 242-259
• 
  Sérgio Vale Aguiar Campos, Edmund M. Clarke: Analysis and Verification of Real-Time Systems Using Quantitative Symbolic Algorithms. 260-269
• 
  Gerard J. Holzmann, Anuj Puri: A Minimized Automaton Representation of Reachable States. 270-278
• 
  Edmund M. Clarke, Orna Grumberg, Marius Minea, Doron Peled: State Space Reduction Using Partial Order Techniques. 279-287
• 
  Carl Pixley, Vigyan Singhal: Model Checking: A Hardware Design Perspective. 288-306

Regular Contribution

• 
  C. Barry Jay: Programming in FISh. 307-315

Volume 2, Number 4, 2000

The Opinion Corner

• 
  George S. Avrunin, James C. Corbett, Matthew B. Dwyer: Benchmarking Finite-State Verifiers. 317-320

Special Section on SPIN

• 
  Gerard J. Holzmann, Elie Najm, Ahmed Serhrouchni: SPIN Model Checking: An Introduction. 321-327
• 
  Yonit Kesten, Amir Pnueli: Control and Data Abstraction: The Cornerstones of Practical Formal Verification. 328-342
• 
  Lynette I. Millett, Tim Teitelbaum: Issues in Slicing PROMELA and Its Applications to Model Checking, Protocol Understanding, and Simulation. 343-349
• 
  Willem Visser, Howard Barringer: Practical CTL^* Model Checking: Should SPIN be Extended? 350-365
• 
  Klaus Havelund, Thomas Pressburger: Model Checking JAVA Programs using JAVA PathFinder. 366-381
• 
  René G. de Vries, Jan Tretmans: On-the-fly Conformance Testing using SPIN. 382-393
• 
  Moataz Kamel, Stefan Leue: Formalization and Validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN. 394-409

Regular Contribution

• 
  Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri: NUSMV: A New Symbolic Model Checker. 410-425