Volume 141, Number 1, 5 December 2005

Proceedings of the First Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode 2005)

• 
  Fausto Spoto: Preface. 1
• 
  Stephen Gilmore, Matthew Prowse: Proof-carrying Bytecode. 3-18
• 
  Martin Wildmoser, Amine Chaieb, Tobias Nipkow: Bytecode Analysis for Proof Carrying Code. 19-34
• 
  Sam Shiel, Ian Bayley: A Translation-Facilitated Comparison Between the Common Language Runtime and the Java Virtual Machine. 35-52
• 
  Walter Binder, Jarle Hulaas: Java Bytecode Transformations for Efficient, Portable CPU Accounting. 53-73
• 
  Alex Buckley, Michelle Murray, Susan Eisenbach, Sophia Drossopoulou: Flexible Bytecode for Linking in .NET. 75-92
• 
  Michael Eichberg: BAT₂XML: XML-based Java Bytecode Representation. 93-107
• 
  Cyrille Artho, Armin Biere: Subroutine Inlining and Bytecode Abstraction to Simplify Static and Dynamic Analysis. 109-128
• 
  Pierre Crégut, Cuihtlauac Alvarado: Improving the Security of Downloadable Java Applications With Static Analysis. 129-144
• 
  René Rydhof Hansen, Igor Siveroni: Towards Verification of Well-Formed Transactions in Java Card Bytecode. 145-162
• 
  Daniel Hedin, David Sands: Timing Aware Information Flow Security for a JavaCard-like Bytecode. 163-182
• 
  Sigmund Cherem, Radu Rugina: A Verifier for Region-Annotated Java Bytecodes. 183-201
• 
  Ian Bayley, Sam Shiel: JVM Bytecode Verification Without Dataflow Analysis. 203-220
• 
  Lucja Kot, Dexter Kozen: Kleene Algebra and Bytecode Verification. 221-236
• 
  Cinzia Bernardeschi, Giuseppe Lettieri, Luca Martini, Paolo Masci: A Space-Aware Bytecode Verifier for Java Cards. 237-254
• 
  Fabian Bannwart, Peter Müller: A Program Logic for Bytecode. 255-273

Volume 141, Number 2, 7 December 2005

Proceedings of the Fourth International Workshop on Compiler Optimization meets Compiler Verification (COCV 2005)

• 
  Jens Knoop, George C. Necula, Wolf Zimmermann: Preface. 1-3
• 
  Hans Langmaack: What Level of Mathematical Reasoning can Computer Science Demand of a Software Implementer?: Auf Deutsch: Welche Art mathematischer Argumentation darf die Informatikwissenschaft einem Softwareimplementierer auf jeden Fall zumuten? 5-32
• 
  Jan Olaf Blech, Sabine Glesner, Johannes Leitner, Steffen Mülling: Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL. 33-51
• 
  Alexandru Salcianu, Konstantine Arkoudas: Machine-Checkable Correctness Proofs for Intra-procedural Dataflow Analyses. 53-68
• 
  Ying Hu, Clark W. Barrett, Benjamin Goldberg, Amir Pnueli: Validating More Loop Optimizations. 69-84
• 
  Andreas Gal, Christian W. Probst, Michael Franz: Structural Encoding of Static Single Assignment Form. 85-102
• 
  Wolfram Amme, Jeffery von Ronne, Michael Franz: Quantifying the Benefits of SSA-Based Mobile Code. 103-119

Volume 141, Number 3, 1 December 2005

Proceedings of the Second International Workshop on Formal Foundations of Embedded Software and Component-based Software Architectures (FESCA 2005)

• 
  Juliana Küster Filipe, Iman Poernomo, Ralf Reussner, Sandeep K. Shukla: Preface. 1-2
• 
  Cristóvão Oliveira, Michel Wermelinger, José Luiz Fiadeiro, Antónia Lopes: Modelling the GSM Handover Protocol in CommUnity. 3-25
• 
  Catherine Menon, Michael Johnson, Charles Lakos: Inconsistency Management and View Updates. 27-51
• 
  Malcolm Wallace: Modular Architectural Representation and Analysis of Fault Propagation and Transformation. 53-71
• 
  Viktoria Firus, Steffen Becker, Jens Happe: Parametric Performance Contracts for QML-specified Software Components. 73-90
• 
  Abdelaziz Guerrouat, Harald Richter: A Formal Approach for Analysis and Testing of Reliable Embedded Systems. 91-106
• 
  Jan Carlson, Mikael Åkerholm: An Event Algebra Extension of the Triggering Mechanism in a Component Model for Embedded Systems. 107-121
• 
  Hartmut Ehrig, Benjamin Braatz, Markus Klein, Fernando Orejas, Sonia Pérez, Elvira Pino: Object-Oriented Connector-Component Architectures. 123-151
• 
  Jean-Paul Bodeveix, David Chemouil, Mamoun Filali, Martin Strecker: Towards formalising AADL in Proof Assistants. 153-169
• 
  Roopak Sinha, Partha S. Roop, Bakhadyr Khoussainov: Adaptive Verification using Forced Simulation. 171-197
• 
  Sotiris Moschoyiannis, Michael W. Shields, Paul J. Krause: Modelling Component Behaviour with Concurrent Automata. 199-220

Volume 141, Number 4, 12 December 2005

Proceedings of the Fifth Workshop on Language Descriptions, Tools, and Applications (LDTA 2005)

• 
  John Tang Boyland, Görel Hedin: Preface. 1-3
• 
  David A. Watt: The Design of Monty: a Programming/Scripting Language. 5-28
• 
  Huiqing Li, Simon J. Thompson, Claus Reinke: The Haskell Refactorer, HaRe, and its API. 29-34
• 
  Dan G. Waddington, Bin Yao: High-Fidelity C/C++ Code Transformation. 35-56
• 
  Timothy Cassidy, James R. Cordy, Thomas R. Dean, Jürgen Dingel: Source Transformation for Concurrency Analysis. 57-75
• 
  Thomas Cleenewerck, Johan Brichau: An Invasive Composition System for Local-to-Global Transformations. 77-98
• 
  Matej Crepinsek, Marjan Mernik, Barrett R. Bryant, Faizan Javed, Alan P. Sprague: Inferring Context-Free Grammars for Domain-Specific Languages. 99-116
• 
  Jochen Kreimer: Adaptive Detection of Design Flaws. 117-136
• 
  Pavel Grigorenko, Ando Saabas, Enn Tyugu: COCOVILA - Compiler-Compiler for Visual Languages. 137-142
• 
  Adrian Johnstone, Elizabeth Scott: Recursion Engineering for Reduction Incorporated Parsers. 143-160
• 
  Mark van den Brand, B. Cornelissen, Pieter A. Olivier, Jurgen J. Vinju: TIDE: A Generic Debugging Framework - Tool Demonstration. 161-165
• 
  Jørgen Iversen: An Action Compiler Targeting Standard ML. 167-188
• 
  Anthony M. Sloane, William M. Waite: Eclipse Support for Using Eli and Teaching Programming Languages. 189-194

Volume 141, Number 5, 22 December 2005

Proceedings of the Workshop on the Foundations of Interactive Computation (FInCo 2005)

• 
  Dina Q. Goldin, Mirko Viroli: Preface. 1-4
• 
  Antônio Carlos da Rocha Costa, Graçaliz Pereira Dimuro: Interactive Computation: Stepping Stone in the Pathway From Classical to Developmental Computation. 5-31
• 
  Mark W. Johnson, Peter McBurney, Simon Parsons: A Mathematical Model of Dialog. 33-48
• 
  L. Gregory Meredith, Matthias Radestock: A Reflective Higher-order Calculus. 49-67
• 
  Leo Motus, Merik Meriste, Walter Dosch: Time-awareness and Proactivity in Models of Interactive Computation. 69-95
• 
  Nigel G. Walker, Marc Wennink: Interactions in Transport Networks. 97-114
• 
  Ian A. Mason, Carolyn L. Talcott: Actors and Logical Analysis of Interactive Systems. 115-133
• 
  Guido Boella, Joris Hulstijn, Leendert W. N. van der Torre: Interaction in Normative Multi-Agent Systems. 135-162
• 
  David Keil, Dina Q. Goldin: Adaptation and Evolution in Dynamic Persistent Environments. 163-179
• 
  Peter Wegner, Farhad Arbab, Dina Q. Goldin, Peter McBurney, Michael Luck, David Robertson: The Role of Agent Interaction in Models of Computing: Panelist Reviews. 181-198