Invited Speakers -- Software Services: Scientific Challenge or Industrial Hype? -- Integrating Variants of DC -- Challenges in Increasing Tool Support for Programming -- A Predicate Spatial Logic and Model Checking for Mobile Processes -- Concurrent and Distributed Systems -- Object Connectivity and Full Abstraction for a Concurrent Calculus of Classes -- Specifying Software Connectors -- Replicative - Distribution Rules in P Systems with Active Membranes -- A Generalisation of a Relational Structures Model of Concurrency -- A Logical Characterization of Efficiency Preorders -- Inherent Causal Orderings of Partial Order Scenarios -- Atomic Components -- Towards an Optimization-Based Method for Consolidating Domain Variabilities in Domain-Specific Web Services Composition -- Model Integration and Theory Unification -- A Formal Framework for Ontology Integration Based on a Default Extension to DDL -- A Predicative Semantic Model for Integrating UML Models -- An Automatic Mapping from Statecharts to Verilog -- Reverse Observation Equivalence Between Labelled State Transition Systems -- Program Reasoning and Testing -- Minimal Spanning Set for Coverage Testing of Interactive Systems -- An Approach to Integration Testing Based on Data Flow Specifications -- Combining Algebraic and Model-Based Test Case Generation -- Verifying OWL and ORL Ontologies in PVS -- Verification -- Symbolic and Parametric Model Checking of Discrete-Time Markov Chains -- Verifying Linear Duration Constraints of Timed Automata -- Idempotent Relations in Isabelle/HOL -- Program Verification Using Automatic Generation of Invariants, -- Theories of Programming and Programming Languages -- Random Generators for Dependent Types -- A Proof of Weak Termination Providing the Right Way to Terminate -- Nelson-Oppen, Shostak and the ExtendedCanonizer: A Family Picture with a Newborn -- Real Time Reactive Programming in Lucid Enriched with Contexts -- Revision Programs with Explicit Negation -- Real-Time and Co-design -- An Algebraic Approach for Codesign -- Duration Calculus: A Real-Time Semantic for B -- An Algebra of Petri Nets with Arc-Based Time Restrictions -- A Calculus for Shapes in Time and Space -- A Framework for Specification and Validation of Real-Time Systems Using Circus Actions -- Automata Theory and Logics -- Switched Probabilistic I/O Automata -- Decomposing Controllers into Non-conflicting Distributed Controllers -- Reasoning About Co-Büchi Tree Automata -- Foundations for the Run-Time Monitoring of Reactive Systems - Fundamentals of the MaC Language -- Tutorials at ICTAC 2004 -- A Summary of the Tutorials at ICTAC 2004.