Volume 190, Number 1, July 2007

Proceedings of the Second Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode 2007)

• 
  Marieke Huisman, Fausto Spoto: Preface. 1
• 
  Jesse McGeachie, Jürgen Dingel: Translate One, Analyze Many: Leveraging the Microsoft Intermediate Language and Source Code Transformation for Model Checking. 3-18
• 
  Emilie Balland, Pierre-Etienne Moreau, Antoine Reilles: Bytecode Rewriting in Tom. 19-33
• 
  Hermann Lehner, Peter Müller: Formal Translation of Bytecode into BoogiePL. 35-50
• 
  Mario Méndez-Lojo, Jorge A. Navas, Manuel V. Hermenegildo: An Efficient, Parametric Fixpoint Algorithm for Analysis of Java Bytecode. 51-66
• 
  Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, Damiano Zanardini: Experiments in Cost Analysis of Java Bytecode. 67-83
• 
  Miguel Gómez-Zamalloa, Elvira Albert, Germán Puebla: Improving the Decompilation of Java Bytecode to Prolog by Partial Evaluation. 85-101
• 
  Ando Saabas, Tarmo Uustalu: Type Systems for Optimizing Stack-based Code. 103-119
• 
  Quan Hoang Nguyen, Bernhard Scholz: Computing SSA Form with Matrices. 121-132
• 
  Jaroslav Sevcík: Proving Resource Consumption of Low-level Programs Using Automated Theorem Provers. 133-147
• 
  Theo C. Ruys, Niels H. M. Aan de Brugh: MMC: the Mono Model Checker. 149-160

Volume 190, Number 2, August 2007

Proceedings of the Third Workshop on Model Based Testing (MBT 2007)

• 
  Bernd Finkbeiner, Yuri Gurevich, Alexander K. Petrenko: Preface. 1
• 
  Sergiy Boroday, Alexandre Petrenko, Roland Groz: Can a Model Checker Generate Tests for Non-Deterministic Systems? 3-19
• 
  Frédéric Dadeau, Yves Ledru, Lydie du Bousquet: Measuring a Java Test Suite Coverage Using JML Specifications. 21-32
• 
  Gordon Fraser, Bernhard K. Aichernig, Franz Wotawa: Handling Model Changes: Regression Testing and Test-Suite Update with Model-Checkers. 33-46
• 
  Anders Hessel, Paul Pettersson: A Global Algorithm for Model-Based Test Suite Generation. 47-59
• 
  Maik Kollmann, Yuen Man Hon: Generating Scenarios by Multi-Object Checking. 61-72
• 
  Yves Ledru, Lydie du Bousquet, Frédéric Dadeau, F. Allouti: A Case Study in Matching Test and Proof Coverage. 73-84
• 
  Martin Ouimet, Kristina Lundqvist: Automated Verification of Completeness and Consistency of Abstract State Machine Specifications using a SAT Solver. 85-97
• 
  Ana C. R. Paiva, João C. P. Faria, Raul F. A. M. Vidal: Towards the Integration of Visual and Formal Models for GUI Testing. 99-111
• 
  Franco Raimondi, Charles Pecheur, Guillaume Brat: Testing Planning Domains (without Model Checkers). 113-125

Volume 190, Number 3, September 2007

Proceedings of the Fifth Workshop on Quantitative Aspects of Programming Languages (QAPL 2007)

• 
  Alessandro Aldini, Franck van Breugel: Preface. 1-2
• 
  Ashok Argent-Katwala, Jeremy T. Bradley: PEPA Queues: Capturing Customer Behaviour in Queueing Networks. 3-25
• 
  Luca Bortolussi, Alberto Policriti: Stochastic Concurrent Constraint Programming and Differential Equations. 27-42
• 
  Vincenzo Ciancia, Gian Luigi Ferrari: Co-Algebraic Models for Quantitative Spatial Logics. 43-58
• 
  Alessandra Di Pierro, Chris Hankin, Herbert Wiklicky: On Probabilistic Techniques for Data Flow Analysis. 59-77
• 
  Tom Chothia, Jun Pang, Muhammad Torabi Dashti: Keeping Secrets in Resource Aware Components. 79-94
• 
  Pedro Baltazar, Paulo Mateus, Rajagopal Nagarajan, Nikolaos Papanikolaou: Exogenous Probabilistic Computation Tree Logic. 95-110
• 
  Stefano Bistarelli, Ugo Montanari, Francesca Rossi, Francesco Santini: Modelling Multicast QoS Routing by using Best-Tree Search in And-or Graphs and Soft Constraint Logic Programming. 111-127
• 
  Michael J. A. Smith: Stochastic Modelling of Communication Protocols from Source Code. 129-145
• 
  Daniele Varacca, Nobuko Yoshida: Probabilistic pi-Calculus and Event Structures. 147-166
• 
  Gagarine Yaikhom, Murray Cole, Stephen Gilmore, Jane Hillston: A Structural Approach for Modelling Performance of Systems Using Skeletons. 167-183
• 
  Yuxin Deng, Wenjie Du: Probabilistic Barbed Congruence. 185-203

Volume 190, Number 4, November 2007

Proceedings of the Workshop on Compiler Optimization meets Compiler Verification (COCV 2007)

• 
  Sabine Glesner, Jens Knoop, Rolf Drechsler: Preface. 1-2
• 
  Roderick Bloem, Stefan J. Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Martin Weiglhofer: Specify, Compile, Run: Hardware from PSL. 3-16
• 
  G. W. Hamilton: Distilling Programs for Verification. 17-32
• 
  María-del-Mar Gallardo, Christophe Joubert, Pedro Merino: On-the-Fly Data Flow Analysis Based on Verification Technology. 33-48
• 
  Ling Fang, Masataka Sassa: Generating Java Compiler Optimizers Using Bidirectional CTL. 49-63
• 
  Jan Olaf Blech, Arnd Poetzsch-Heffter: A Certifying Code Generation Phase. 65-82