Volume 5, Number 1, November 2003

Special section on trends in verification and validation

• 
  Tiziana Margaria, Wang Yi: Introductory paper: scalability aspects of validation. 1-3
• 
  Poul Frederick Williams, Henrik Reif Andersen, Henrik Hulgaard: Satisfiability checking using Boolean Expression Diagrams. 4-14
• 
  Tuba Yavuz-Kahveci, Tevfik Bultan: A symbolic manipulator for automated verification of reactive systems with heterogeneous data types. 15-33
• 
  Corina S. Pasareanu, Matthew B. Dwyer, Willem Visser: Finding feasible abstract counter-examples. 34-48
• 
  Thomas Ball, Andreas Podelski, Sriram K. Rajamani: Boolean and Cartesian abstraction for model checking C programs. 49-58
• 
  Brian Nielsen, Arne Skou: Automated test generation from timed automata. 59-77
• 
  Elsa L. Gunter, Anca Muscholl, Doron Peled: Compositional message sequence charts. 78-89

Regular contribution

• 
  Philippe Chevalley, Pascale Thévenod-Fosse: A mutation analysis tool for Java programs. 90-103

Volume 5, Number 2-3, March 2004

• 
  Jaco van de Pol: Introductory paper. 105-106
• 
  Tiziana Margaria, Bernhard Steffen: Lightweight coarse-grained coordination: a scalable system-level approach. 107-123
• 
  David Lugato, Céline Bigot, Yannick Valot, Jean-Pierre Gallois, Sébastien Gérard, François Terrier: Validation and automatic test generation on UML models: the AGATHA approach. 124-139
• 
  Alexander Pretschner, Oscar Slotosch, Ernst Aiglstorfer, Stefan Kriebel: Model-based testing for real. 140-157
• 
  Gordon J. Pace, Nicolas Halbwachs, Pascal Raymond: Counter-example generation in symbolic abstract model-checking. 158-164
• 
  María-del-Mar Gallardo, Jesús Martínez, Pedro Merino, Ernesto Pimentel: aSPIN: A tool for abstract model checking. 165-184
• 
  Viktor Schuppan, Armin Biere: Efficient reduction of finite state model checking to reachability analysis. 185-204
• 
  Thomas Arts, Clara Benac Earle, John Derrick: Development of a verified Erlang program for resource locking. 205-220
• 
  Conrado Daws, Marta Z. Kwiatkowska, Gethin Norman: Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM. 221-236
• 
  Sylvie Boldo, Marc Daumas: Properties of two's complement floating point notations. 237-246
• 
  Stefan Edelkamp, Stefan Leue, Alberto Lluch-Lafuente: Directed explicit-state model checking in the validation of communication protocols. 247-267
• 
  Giorgio Delzanno, Jean-François Raskin, Laurent Van Begin: Covering sharing trees: a compact data structure for parameterized verification. 268-297

Volume 5, Number 4, May 2004

• 
  S. Purushothaman Iyer, David Hislop, Paul L. Jones, Jaime Lee, Frederick Pearce, Stephen Van Albert: Introductory paper. 299-300
• 
  John C. Martin: Formal methods software engineering for the CARA system. 301-307
• 
  Rajeev Alur, David Arney, Elsa L. Gunter, Insup Lee, Jaime Lee, Wonhong Nam, Frederick Pearce, Stephen Van Albert, Jiaxiang Zhou: Formal specifications and analysis of the computer-assisted resuscitation algorithm (CARA) Infusion Pump Control System. 308-319
• 
  Raoul Praful Jetley, Cohan Carlos, S. Purushothaman Iyer: A case study on applying formal methods to medical devices: computer-aided resuscitation algorithm. 320-330
• 
  Eugene W. Stark: Formally specifying CARA in Java. 331-350
• 
  Arnab Ray, Rance Cleaveland: Unit verification: the CARA experience. 351-369
• 
  Luqi, Zhiwei Guan, Valdis Berzins, Lynn Zhang, David L. Floodeen, Vedat Coskun, Joseph Puett, Michael Brown: Requirements-document-based prototyping of CARA software. 370-390