Shape Analysis / Reinhard Wilhelm ; Mooly Sagiv ; Thomas Reps
Optimizing Java Bytecode Using the Soot Framework: Is It Feasible? / Raja Vallee-Rai ; Etienne Gagnon ; Laurie Hendren ; Patrick Lam ; Patrice Pominville ; Vijay Sundaresan
Automatic Removal of Array Memory Leaks in Java / Ran Shaham ; Elliot K. Kolodner
A Static Study of Java Exceptions Using JESP / Barbara G. Ryder ; Donald Smith ; Ulrich Kremer ; Michael Gordon ; Nirav Shah
Fast Escape Analysis and Stack Allocation for Object-Based Programs / David Gay ; Bjarne Steensgaard
Constant Propagation on the Value Graph: Simple Constants and Beyond / Jens Knoop ; Oliver Ruthing
Simple Generation of Static Single-Assignment Form / John Aycock ; Nigel Horspool
Demand-Driven Construction of Call Graphs / Gagan Agrawal
A Framework for Loop Distribution on Limited On-Chip Memory Processors / Lei Wang ; Waibhav Tembe ; Santosh Pande
Techniques for Effectively Exploiting a Zero Overhead Loop Buffer / Gang-Ryung Uh ; Yuhong Wang ; David Whalley ; Sanjay Jinturkar ; Chris Burns ; Vincent Cao
Advanced Compiler Optimization for CalmRISC8 Low-End Embedded Processor / Dae-Hwan Kim
Global Software Pipelining with Iteration Preselection / David Gregg
Analysis of Irregular Single-Indexed Array Accesses and Its Applications in Compiler Optimizations / Yuan Lin ; David Padua
Advanced Scalarization of Array Syntax / Gerald Roth
Techniques for Reducing the Overhead of Run-Time Parallelization / Hao Yu ; Lawrence Rauchwerger
MATOU: An Implementation of Mode-Automata / Florence Maraninchi ; Yann Remond ; Yannick Raoul
Compiling Adaptive Programs by Partial Evaluation / Peter Thiemann
Shape Analysis / Reinhard Wilhelm ; Mooly Sagiv ; Thomas Reps
Optimizing Java Bytecode Using the Soot Framework: Is It Feasible? / Raja Vallee-Rai ; Etienne Gagnon ; Laurie Hendren ; Patrick Lam ; Patrice Pominville ; Vijay Sundaresan
An Essay on Software Engineering at the Turn of Century / Wladyslaw M. Turski
Memex Is Not Enough / Richard Mark Soley
From Play-In Scenarios to Code: An Achievable Dream / David Harel
Real-Time Systems
Parallel Refinement Mechanisms for Real-Time Systems / Paul Z. Kolano ; Richard A. Kemmerer ; Dino Mandrioli
Applying RT-Z to Develop Safety-Critical Systems / Carsten Sühl
A Process Algebra for Real-Time Programs / Henning Dierks
Formally Engineering Systems
System Fault Tolerance Specification: Proposal of a Method Combining Semi-formal and Formal Approaches / Giovanna Dondossola ; Oliver Botti
Structuring and Design of Reactive Systems Using RSDS and B / K. Lano ; K. Androutsopoulos ; D. Clark
Using Domain-Specific Languages for the Realization of Component Composition / Matthias Anlauff ; Philipp W. Kutter ; Alfonso Pierantonio ; Asuman Sünbül
Software Engineering
Analysing UML Active Classes and Associated State Machines - A Lightweight Formal Approach / G. Reggio ; E. Astesiano ; C. Choppy ; H. Hussmann
What Is 'Mathematicalness' in Software Engineering? / Hidetaka Kondoh
A Formal Approach to Heterogeneous Software Modeling / Alexander Egyed ; Nenad Medvidovic
Object Orientation
Formal Specification of Object-Oriented Meta-modelling / Gunnar Övergaard
Verification of Object Oriented Programs Using Class Invariants / Kees Huizing ; Ruurd Kuiper ; SOOP
Verification of Object-Z Specifications by Using Transition Systems: Application to the Radiomobile Network Design Problem / Pablo Gruer ; Vincent Hilaire ; Abder Koukam
A Model for Describing Object-Oriented Systems from Multiple Perspectives / Torsten Nelson ; Donald Cowan ; Paulo Alencar
Stepwise Introduction and Preservation of Safety Properties in Algebraic High-Level Net Systems / J. Padberg ; K. Hoffmann ; M. Gajewsky
Theory and Applications
Ready-Simulation Is Not Ready to Express a Modular Refinement Relation / Françoise Bellegarde ; Jacques Julliand ; Olga Kouchnarenko
Java Program Verification via a Hoare Logic with Abrupt Termination / Marieke Huisman ; Bart Jacobs
Foundations for Software Configuration Management Policies Using Graph Transformations / Francesco Parisi-Presicce ; Alexander L. Wolf
On the Construction of Automata from Linear Arithmetic Constraints / Pierre Wolper ; Bernard Boigelot
Software and Formal Methods Tools
An Extensible Type Systemfor Component-Based Design / Yuhong Xiong ; Edward A. Lee
Proof General: A Generic Tool for Proof Development / David Aspinall
ViewPoint-Oriented Software Development: Tool Support for Integrating Multiple Perspectives by Distributed Graph Transformation / Michael Goedicke ; Bettina Enders ; Torsten Meyer ; Gabriele Taentzer
Formal Methods Tools
Consistent Integration of Formal Methods / Peter Braun ; Heiko Lötzbeyer ; Bernhard Schätz ; Oscar Slotosch
An Architecture for Interactive Program Provers / Jörg Meyer ; Arnd Poetzsch-Heffter
The PROSPER Toolkit / Louise A. Dennis ; Graham Collins ; Michael Norrish ; Richard Boulton ; Konrad Slind ; Graham Robinson ; Mike Gordon ; Tom Melham
CASL: From Semantics to Tools / Till Mossakowski
Timed and Hybrid Systems
On the Construction of Live Timed Systems / Sébastien Bornot ; Gregor Gößler ; Joseph Sifakis
On Memory-Block Traversal Problems in Model-Checking Timed Systems / Fredrik Larsson ; Paul Pettersson ; Wang Yi
Symbolic Model Checking for Rectangular Hybrid Systems / Thomas A. Henzinger ; Rupak Majumdar
Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems / Farn Wang
Infinite and Parameterized Systems
Verification of Parameterized Systems Using Logic Program Transformations / Abhik Roychoudhury ; K. Narayan Kumar ; C.R. Ramakrishnan ; I. V. Ramakrishnan ; Scott A. Smolka
Abstracting WS1S Systems to Verify Parameterized Networks / Kai Baukus ; Saddek Bensalem ; Yassine Lakhnech ; Karsten Stahl
FMona: A Tool for Expressing Validation Techniques over Infinite State Systems / J.-P. Bodeveix ; M. Filali
Transitive Closures of Regular Relations for Verifying Infinite-State Systems / Bengt Jonsson ; Marcus Nilsson
Diagnostic and Test Generation
Using Static Analysis to Improve Automatic Test Generation / Marius Bozga ; Jean-Claude Fernandez ; Lucian Ghirvu
Efficient Diagnostic Generation for Boolean Equation Systems / Radu Mateescu
Efficient Model-Checking
Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems / Jean-Pierre Krimm ; Laurent Mounier
Checking for CFFD-Preorder with Tester Processes / Juhana Helovuo ; Antti Valmari
Fair Bisimulation / Sriram K. Rajamani
Integrating Low Level Symmetries into Reachability Analysis / Karsten Schmidt
Model-Checking Tools
Model Checking Support for the ASM High-Level Language / Giuseppe Del Castillo ; Kirsten Winter
A Markov Chain Model Checker / Holger Hermanns ; Joost-Pieter Katoen ; Joachim Meyer-Kayser ; Markus Siegle
Model Checking SDL with Spin / Dragan Bošnački ; Dennis Dams ; Leszek Holenderski ; Natalia Sidorova
Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking / Ramesh Bharadwaj ; Steve Sims
Symbolic Model-Checking
Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation / Luca de Alfaro ; Marta Kwiatkowska ; Gethin Norman ; David Parker ; Roberto Segala
Symbolic Reachability Analysis Based on SAT-Solvers / Parosh Aziz Abdulla ; Per Bjesse ; Niklas Eén
Symbolic Representation of Upward-Closed Sets / Giorgio Delzanno ; Jean-François Raskin
BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems / Tevfik Bultan
Visual Tools
Tool-Based Specification of Visual Languages and Graphic Editors / Magnus Niemann ; Roswitha Bardohl
VIP: A Visual Editor and Compiler for v-Promela / Moataz Kamel ; Stefan Leue
Verification of Critical Systems
A Comparison of Two Verification Methods for Speculative Instruction Execution / Tamarah Arons ; Amir Pnueli
Partial Order Reductions for Security Protocol Verification / Edmund Clarke ; Somesh Jha ; Will Marrero
Model Checking Security Protocols Using a Logic of Belief / Massimo Benerecetti ; Fausto Giunchiglia
A Formal Specification and Validation of a Critical System in Presence of Byzantine Errors / S. Gnesi ; D. Latella ; G. Lenzini ; C. Abbaneo ; A. Amendola ; P. Marmo
Author Index
Invited Contribution
On the Construction of Automata from Linear Arithmetic Constraints / Pierre Wolper ; Bernard Boigelot
LISA: An Interactive Environment for Programming Language Development / Marjan Mernik ; Mitja Lenič ; Enis AvdičauÜević ; Viljem Äumer
Building an Interpreter with Vmgen / M. Anton Ertl ; David Gregg
Compiler Construction Using LOTOS NT / Hubert Garavel ; Frédéric Lang ; Radu Mateescu
Analysis and Optimization
Data Compression Transformations for Dynamically Allocated Data Structures / Youtao Zhang ; Rajiv Gupta
Evaluating a Demand Driven Technique for Call Graph Construction / Gagan Agrawal ; Jinqian Li ; Qi Su
A Graph-Free Approach to Data-Flow Analysis / Markus Mohnen
A Representation for Bit Section Based Analysis and Optimization / Eduard Mehofer
A Comprehensive Approach to Array Bounds Check Elimination for Java / Feng Qian ; Clark Verbrugge
Author Index
Tool Demonstrations
LISA: An Interactive Environment for Programming Language Development / Marjan Mernik ; Mitja Lenič ; Enis AvdičauÜević ; Viljem Äumer
Building an Interpreter with Vmgen / M. Anton Ertl ; David Gregg
A Generic Component Framework for System Modeling / Hartmut Ehrig ; Fernando Orejas ; Benjamin Braatz ; Markus Klein ; Martti Piirainen
Model and Program Analysis
Implementing Condition/Event Nets in the Circal Process Algebra / Antonio Cerone
Integrated State Space Reduction for Model Checking Executable Object-Oriented Software System Designs / Fei Xie ; James C. Browne
Model Generation by Moderated Regular Extrapolation / Andreas Hagerer ; Hardi Hungar ; Oliver Niese ; Bernhard Steffen
Better Slicing of Programs with Jumps and Switches / Sumit Kumar ; Susan Horwitz
Architecture Descriptions
Architectural Types Revisited: Extensible And/Or Connections / Marco Bernardo ; Francesco Franzè
Mapping an ADL to a Component-Based Application Development Environment / VirgÆinia C.C. de Paula ; Thais V. Batista
From EDOC to CCM Components: A Precise Mapping Specification / Mariano Belaunde ; Mikael Peltier
Meta-Models
Engineering Modelling Languages: A Precise Meta-Modelling Approach / Tony Clark ; Andy Evans ; Stuart Kent
A Toolbox for Automating Visual Software Engineering / Juan de Lara ; Hans Vangheluwe ; Luciano Baresi ; Mauro Pezzè
Formal Approaches towards UML
Enriching OCL Using Observational Mu-Calculus / Julian Bradfield ; Juliana Küster Filipe ; Perdita Stevens
Formal Verification of UML Statecharts with Real-Time Extensions / Alexandre David ; M. Oliver Möller ; Wang Yi
Requirements Engineering
An Authoring Tool for Informal and Formal Requirements Specifications / Reiner Hähnle ; Kristofer Johannisson ; Aarne Ranta
Introducing Context-Based Constraints / Felix Bübl
Formal Requirements Engineering Using Observer Models / Andreas Nonnengart ; Georg Rock ; Werner Stephan
Automatic Generation of Use Cases from Workflows: A Petri Net Based Approach / Oscar López ; Miguel A. Laguna ; Francisco J. GarcÃa
Meta-modeling Techniques Meet Web Application Design Tools / Franca Garzotto ; Luca Mainetti ; Paolo Paolini
Formal-Driven Conceptualization and Prototyping of Hypermedia Applications / Antonio Navarro ; Baltasar Fernandez-Manjon ; Alfredo Fernandez-Valmayor ; Jose Luis Sierra
The Key System: Integrating Object-Oriented Design and Formal Methods / Wolfgang Ahrendt ; Thomas Baar ; Bernhard Beckert ; Martin Giese ; Elmar Habermalz ; Wolfram Menzel ; Wojciech Mostowski ; Peter H. Schmitt
ObjectCheck: A Model Checking Tool for Executable Object-Oriented Software System Designs / Vladimir Levin
Demonstration of an Operational Procedure for the Model-Based Testing of CTI Systems / Tiziana Margaria ; Oliver Niese,Bernhard Steffen ; Hans-Dieter Ide
Author Index
Formal Frameworks
An Approach to Composition Motivated by wp / Michel Charpentier
Symbiosis of Static Analysis and Program Testing / Michal Young
Software Components
An Ontology for Software Component Matching / Claus Pahl
A Description Language for Composable Components / Ioana Şora ; Pierre Verbaeten ; Yolande Berbers
A Logical Basis for the Specification of Reconfigurable Component-Based Systems / Nazareno Aguirre ; Tom Maibaum
An Overall System Design Approach Doing Object-Oriented Modeling to Code-Generation for Embedded Electronic Systems / Clemens Reichmann ; Markus Kühl ; Klaus D. Müller-Glaser
Mobile Computing
Composing Specifications of Event Based Applications / Pascal Fenkam ; Harald Gall ; Mehdi Jazayeri
A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems / Stephan Merz ; Martin Wirsing ; Júlia Zappe
Spatial Security Policies for Mobile Agents in a Sentient Computing Environment / Davit Scott ; Alastair Beresford ; Alan Mycroft
Aspect and Object-Oriented Programming
Towards UML-Based Formal Specifications of Component-Based Real-Time Software / Vieri Del Bianco ; Luigi Lavazza ; Marco Mauri ; Giuseppe Occorso
Modelling Recursive Calls with UML State Diagrams / Jennifer Tenzer ; Perdita Stevens
Pipa: A Behavioral Interface Specification Language for AspectJ / Jianjun Zhao ; Martin Rinard
PacoSuite and JAsCo: A Visual Component Composition Environment with Advanced Aspect Separation Features / Wim Vanderperren ; Davy Suvée ; Bart Wydaeghe ; Viviane Jonckers
Distributed and Web Applications
Model-Based Development of Web Applications Using Graphical Reaction Rules / Reiko Heckel ; Marc Lohmann
Modular Analysis of Dataflow Process Networks / Yan Jin ; Robert Esser ; Charles Lakos ; Jörn W. Janneck
Software Measurements
Foundations of a Weak Measurement-Theoretic Approach to Software Measurement / Sandro Morasca
An Information-Based View of Representational Coupling in Object-Oriented Systems / Pierre Kelsen
Formal Verification
A Temporal Approach to Specification and Verification of Pointer Data-Structures / Marcin Kubica
A Program Logic for Handling Java Card's Transaction Mechanism / Bernhard Beckert ; Wojciech Mostowski
Monad-Independent Hoare Logic in HasCASL / Lutz Schröder ; Till Mossakowski
Visual Specifications of Policies and Their Verification / Manuel Koch ; Francesco Parisi-Presicce
Analysis and Testing
Automatic Model Driven Animation of SCR Specifications / Angelo Gargantini ; Elvinia Riccobene
Model Checking Software via Abstraction of Loop Transitions / Natasha Sharygina ; James C. Browne
Model Integrations and Extensions
Integration of Formal Datatypes within State Diagrams / Christian Attiogbé ; Pascal Poizat ; Gwen Salaün
Xere: Towards a Natural Interoperability between XML and ER Diagrams / Giuseppe Della Penna ; Antinisca Di Marco ; Benedetto Intrigila ; Igor Melatti ; Alfonso Pierantonio
Detecting Implied Scenarios Analyzing Non-local Branching Choices / Henry Muccini
Capturing Overlapping, Triggered, and Preemptive Collaborations Using MSCs / Ingolf H. Krüger
Author Index
Keynote
Symbiosis of Static Analysis and Program Testing / Michal Young
Integrating High-Level Optimizations in a Production Compiler: Design and Implementation Experience / Somnath Ghosh ; Abhay Kanhere ; Rakesh Krishnaiyer ; Dattatraya Kulkarni ; Wei Li ; Chu-Cheow Lim ; John Ng
Improving Data Locality by Chunking / Cedric Bastoul ; Paul Feautrier
Author Index
Register Allocation
Combined Code Motion and Register Allocation Using the Value State Dependence Graph / Neil Johnson ; Alan Mycroft
Early Control of Register Pressure for Software Pipelined Loops / Sid-Ahmed-Ali Touati ; Christine Eisenbeis
Physical Programming: Beyond Mere Logic (Invited Talk) / Bran Selic
Metamodelling
Metamodelling and Conformance Checking with PVS / Richard F. Paige ; Jonathan S. Ostroff
The Metamodelling Language Calculus: Foundation Semantics for UML / Tony Clark ; Andy Evans ; Stuart Kent
Distributed Components
Compositional Checking of Communication among Observers / Ralf Pinger ; Hans-Dieter Ehrich
Combining Independent Specifications / Joy N. Reed ; Jane E. Sinclair
Proving Deadlock Freedom in Component-Based Programming / Paola Inverardi ; Sebastian Uchitel
UML
A Real-Time Execution Semantics for UML Activity Diagrams / Rik Eshuis ; Roel Wieringa
A CSP View on UML-RT Structure Diagrams / Clemens Fischer ; Ernst-Rüdiger Olderog ; Heike Wehrheim
Strengthening UML Collaboration Diagrams by State Transformations / Reiko Heckel ; Stefan Sauer
Specification of Mixed Systems in Korrigan with the Support of a UML-Inspired Graphical Notation / Christine Choppy ; Pascal Poizat ; Jean-Claude Royer
On Use Cases and Their Relationships in the Unified Modelling-Language / Perdita Stevens
On the Importance of Inter-scenario Relationships in Hierarchical State Machine Design / Francis Bordeleau ; Jean-Pierre Corriveau
Towards a Rigorous Semantics of UML Supporting Its Multiview Approach / Gianna Reggio ; Maura Cerioli ; Egidio Astesiano
Towards Development of Secure Systems Using UMLsec / Jan Jürjens
Testing
Grammar Testing / Ralf Lämmel
Debugging via Run-Time Type Checking / Alexey Loginov ; Suan Hsi Yong ; Susan Horwitz ; Thomas Reps
Library-Based Design and Consistency Checking of System-Level Industrial Test Cases / Oliver Niese ; Bernhard Steffen ; Tiziana Margaria ; Andreas Hagerer ; Georg Brune ; Hans-Dieter Ide
Demonstration of an Automated Integrated Testing Environment for CTI Systems / Markus Nagelmann ; Klaus Kolodziejczyk-Strunck ; Werner Goerigk ; Andrei Erochok ; Bernhard Hammelmann
Formal Methods
Semantics of Architectural Specifications in CASL / Lutz Schröder ; Till Mossakowski ; Andrzej Tarlecki ; Bartek Klin ; Piotr Hoffman
Extending Development Graphs with Hiding / Serge Autexier ; Dieter Hutter
A Logic for the Java Modeling Language JML / Bart Jacobs ; Erik Poll
A Hoare Calculus for Verifying Java Realizations of OCL-Constrained Design Models / Bernhard Reus ; Martin Wirsing ; Rolf Hennicker
Case Studies
A Formal Object-Oriented Analysis for Software Reliability: Design for Verification / Natasha Sharygina ; James C. Browne ; Robert P. Kurshan
Specification and Analysis of the AER/NCA Active Network Protocol Suite in Real-Time Maude / Peter C. Ölveczky ; Mark Keaton ; Jose Meseguer ; Carolyn Talcott ; Steve Zabele
Author Index
Invited Paper
Physical Programming: Beyond Mere Logic (Invited Talk) / Bran Selic
SmartTools: A Generator of Interactive Environments Tools / Isabelle Attali ; Carine Courbis ; Pascal Degenne ; Alexandre Fau ; Didier Parigot ; Claude Pasquier
Visual Patterns in the VLEli System / Matthias T. Jung ; Uwe Kastens ; Christian Schindler ; Carsten Schmidt
The Asf=Sdf Meta-environment: A Component-Based Language Development Environment / M.G.J. van den Brand ; A. van Deursen ; J. Heering ; H.A. de Jong ; M. de Jonge ; T. Kuipers ; P. Klint ; L. Moonen ; P.A. Olivier ; J. Scheerder ; J.J. Vinju ; E. Visser ; J. Visser
Author Index
Invited Talk
Virtual Classes and Their Implementation / Ole Lehrman Madsen
Adequacy for Algebraic Effects / Gordon Plotkin ; John Power
Contributed Papers
Secrecy Types for Asymmetric Communication / MartÆin Abadi ; Bruno Blanchet
Axiomatizing Tropical Semirings / Luca Aceto ; Zoltán Ésik ; Anna Ingólfsdóttir
Type Isomorphisms and Proof Reuse in Dependent Type Theory / Gilles Barthe ; Olivier Pons
On the Duality between Observability and Reachability / Michel Bidoit ; Rolf Hennicker ; Alexander Kurz
The Finite Graph Problem for Two-Way Alternating Automata / Mikolaj Bojanczyk
High-Level Petri Nets as Type Theories in the Join Calculus / Maria Grazia Buscemi ; Vladimiro Sassone
Temporary Data in Shared Dataspace Coordination Languages / Nadia Busi ; Roberto Gorrieri ; Gianluigi Zavattaro
On Garbage and Program Logic / Cristiano Calcagno ; Peter W. O'Hearn
The Complexity of Model Checking Mobile Ambients / Witold Charatonik ; Silvano Dal Zilio ; Andrew D. Gordon ; Supratik Mukhopadhyay ; Jean-Marc Talbot
The Rho Cube / Horatiu Cirstea ; Claude Kirchner ; Luigi Liquori
Type Inference with Recursive Type Equations / Mario Coppo
On the Modularity of Deciding Call-by-Need / Irène Durand ; Aart Middeldorp
Synchronized Tree Languages Revisited and New Applications / Valèrie Gouranton ; Pierre Rèty ; Helmut Seidl
Computational Completeness of Programming Languages Based on Graph Transformation / Annegret Habel ; Detlef Plump
Axioms for Recursion in Call-by-Value (Extended Abstract) / Masahito Hasegawa ; Yoshihiko Kakutani
Class Analysis of Object-Oriented Programs through Abstract Interpretation / Thomas Jensen ; Fausto Spoto
On the Complexity of Parity Word Automata / Valerie King ; Orna Kupferman ; Moshe Y. Vardi
Foundations for a Graph-Based Approach to the Specification of Access Control Policies / Manuel Koch ; Luigi Vincenzo Mancini ; Francesco Parisi-Presicce
Categories of Processes Enriched in Final Coalgebras / Sava Krstić ; John Launchbury ; DuÜko Pavlovič
Model Checking CTL= and FCTL Is Hard / François Laroussinie ; Nicolas Markey ; Philippe Schnoebelen
On Regular Message Sequence Chart Languages and Relationships to Mazurkiewicz Trace Theory / Rémi Morin
Verified Bytecode Verifiers / Tobias Nipkow
Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the p-Calculus and Mechanizing the Theory of Contexts / Christine Röckl ; Daniel Hirschkoff ; Stefan Berghofer
Decidability of Weak Bisimilarity for a Subset of Basic Parallel Processes / Colin Stirling
An Axiomatic Semantics for the Synchronous Language Gentzen / Simone Tini
Tool Presentation
Marrella and the Verification of an Embedded System / Dominique Ambroise ; Patrick Augé ; Kamel Bouchefra ; Brigitte Rozoy
Author Index
Invited Paper
Adequacy for Algebraic Effects / Gordon Plotkin ; John Power
An Automata Based Interpretation of Live Sequence Charts|CJ. Klose|CH. Wittke
Logics and Model-Checking
Coverage Metrics for Temporal Logic Model Checking|CH. Chockler|CO. Kupferman|CM. Y. Vardi
Parallel Model Checking for the Alternation Free $$-Calculus|CB. Bollig / CM. Leucker ; M. Weber
Model Checking CTL*[DC] / P.K. Pandya
ETAPS Tool Demonstration
CPN/Tools: A Tool for Editing and Simulating Coloured Petri Nets ETAPS Tool Demonstration Related to TACAS / M. Beaudomn-Lafon ; W.E. Mackay ; M. Jensen ; P. Andersen ; P. Janecek ; M. Lassen ; K. Lund ; K. Mortensen ; S. Munck ; A. Ratzer ; K. Ravn ; K. Jensen
The ASM Workbench: A Tool Environment for Computer-Aided Analysis and Validation of Abstract State Machine Models / G. Del Castillo
The Erlang Verification Tool / T. Noll ; L. Fredlund ; D. Gurov
Author Index
Invited Contributions
Branching vs. Linear Time: Final Showdown / M.Y. Vardi
Trust Management in Strand Spaces: A Rely-Guarantee Method / Joshua D. Guttman ; F. Javier Thayer ; Jay A. Carlson ; Jonathan C. Herzog ; John D. Ramsdell ; Brian T. Sniffen
Checking Absence of Illicit Applet Interactions: A Case Study / Marieke Huisman ; Dilian Gurov ; Christoph Sprenger ; Gennady Chugunov
A Tool-Assisted Framework for Certified Bytecode Verification / Gilles Barthe ; Guillaume Dufay
Reasoning about Card Tears and Transactions in Java Card / Engelbert Hubbers ; Erik Poll
Components I
Predictable Dynamic Plugin Systems / Robert Chatley ; Susan Eisenbach ; Jeff Kramer ; Jeff Magee ; Sebastian Uchitel
A Correlation Framework for the CORBA Component Model / Georg Jung ; John Hatcliff ; Venkatesh Prasad Ranganath
Cadena: An Integrated Development Environment for Analysis, Synthesis, and Verification of Component-Based Systems / Adam Childs ; Jesse Greenwald ; Xianghua Deng ; Matthew Dwyer ; Prashant Shanti ; Gurdip Singh
Security and Web Services
Actor-Centric Modeling of User Rights / Ruth Breu ; Gerhard Popp
Modeling Role-Based Access Control Using Parameterized UML Models / Dae-Kyoo Kim ; Indrakshi Ray ; Robert France ; Na Li
Compositional Nested Long Running Transactions / Laura Bocchi
DaGen: A Tool for Automatic Translation from DAML-S to High-Level Petri Nets / Daniel Moldt ; Jan Ortmann
Modeling and Requirements
Integrating Meta-modelling Aspects with Graph Transformation for Efficient Visual Language Definition and Model Manipulation / Roswitha Bardohl ; Hartmut Ehrig ; Juan de Lara ; Gabriele Taentzer
An Operational Semantics for Stateflow / Grégoire Hamon ; John Rushby
Improving Use Case Based Requirements Using Formally Grounded Specifications / Christine Choppy ; Gianna Reggio
The GOPCSD Tool: An Integrated Development Environment for Process Control Requirements and Design / Islam A.M. El-Maddah ; Tom S.E. Maibaum
Testing
Automated Debugging Using Path-Based Weakest Preconditions / Haifeng He ; Neelam Gupta
Filtering TOBIAS Combinatorial Test Suites / Yves Ledru ; Lydie du Bousquet ; Olivier Maury ; Pierre Bontron
Systematic Testing of Software Architectures in the C2 Style / Henry Muccini ; Marcio Dias ; Debra J. Richardson
Model Checking and Analysis
Optimising Communication Structure for Model Checking / Peter Saffrey ; Muffy Calder
Translating Software Designs for Model Checking / Fei Xie ; Vladimir Levin ; Robert P. Kurshan ; James C. Browne
Enhancing Remote Method Invocation through Type-Based Static Analysis / Carlo Ghezzi ; Vincenzo Martena ; Gian Pietro Picco
Specification and Analysis of Real-Time Systems Using Real-Time Maude / Peter Csaba Ölveczky ; José Meseguer
Components II
A Systematic Methodology for Developing Component Frameworks / Si Won Choi ; Soo Ho Chang ; Soo Dong Kim
Automating Decisions in Component Composition Based on Propagation of Requirements / Ioana Şora ; Vladimir Creţu ; Pierre Verbaeten ; Yolande Berbers
Author Index
Invited Contributions
Distributed Information Management with XML and Web Services / Serge Abiteboul
A Formal Treatment of Context-Awareness / Gruia-Catalin Roman ; Christine Julien ; Jamie Payton