1. MEMOCODE 2003: Mont Saint-Michel, France

Invited Talk

• José Meseguer:
  Executable Computational Logics: Combining Formal Methods and Programming Language Based System Design. 3-
  Electronic Edition (link) BibTeX

System Level Models and Co-design

• Jan Romberg, Oscar Slotosch, Gabor Hahn:
  MoDe: A Method for System-Level Architecture Evaluation. 13-23
  Electronic Edition (link) BibTeX
• Luís Gomes, Anikó Costa:
  From Use Cases to System Implementation: Statechart Based Co-design. 24-33
  Electronic Edition (link) BibTeX
• Julio A. de Oliveira Filho, Manoel Eusebio de Lima, Paulo Romero Martins Maciel:
  Petri Net Based Interface Analysis for Fast IP-Core Integration. 34-
  Electronic Edition (link) BibTeX

Short Presentation Session

• Islam A. M. El-Maddah, T. S. E. Maibaum:
  Goal-Oriented Requirements Analysis for Process Control Systems Design. 45-46
  Electronic Edition (link) BibTeX
• Sander Stuijk, Twan Basten:
  Analyzing Concurrency in Computational Networks. 47-48
  Electronic Edition (link) BibTeX
• Margot Bittner, Florian Kammüller:
  Translating Fusion/UML to Object-Z. 49-50
  Electronic Edition (link) BibTeX
• Görschwin Fey, Rolf Drechsler:
  Finding Good Counter-Examples to Aid Design Verification. 51-
  Electronic Edition (link) BibTeX

Formal Verification I

• Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang:
  High Level Verification of Control Intensive Systems Using Predicate Abstraction. 55-64
  Electronic Edition (link) BibTeX
• Sudarshan K. Srinivasan, Miroslav N. Velev:
  Formal Verification of an Intel XScale Processor Model with Scoreboarding, Specialized Execution Pipelines, and Impress Data-Memory Exceptions. 65-74
  Electronic Edition (link) BibTeX
• Magali Contensin, Laurence Pierre:
  Combining ACL2 and a v-calculus Model-Checker to Verify System-Level Designs. 75-
  Electronic Edition (link) BibTeX

Field Modifiability and Verifiability

• Hiroshi Saito, Kenshu Seto, Yoshihisa Kojima, Satoshi Komatsu, Masahiro Fujita:
  Engineering Changes in Field Modifiable Architectures. 87-94
  Electronic Edition (link) BibTeX

Panel I

• Grant Martin, Sandeep K. Shukla:
  Hierarchical and Incremental Verification for System Level Design: Challenges and Accomplishments. 97-
  Electronic Edition (link) BibTeX

Refinement/Conformance I

• Françoise Bellegarde, Celina Charlet, Olga Kouchnarenko:
  How to Compute the Refinement Relation for Parameterized Systems. 103-112
  Electronic Edition (link) BibTeX
• Thierry J.-F. Omnés, Gerard Postuma, Jos Verhaegh, Marleen Boonen, Nick Gatherer:
  Using SSDE for USB2.0 conformance co-verification. 113-122
  Electronic Edition (link) BibTeX
• Thierry Grandpierre, Yves Sorel:
  From Algorithm and Architecture Specifications to Automatic Generation of Distributed Real-Time Executives: a Seamless Flow of Graphs Transformations. 123-
  Electronic Edition (link) BibTeX

Invited Talk

• Kenneth L. McMillan:
  Methods for exploiting SAT solvers in unbounded model checking. 135-
  Electronic Edition (link) BibTeX

Validation, Co-validation

• Franco Fummi, Graziano Pravadelli, Andrea Fedeli, Umberto Rossi, Franco Toto:
  On the Use of a High-Level Fault Model to Check Properties Incompleteness. 145-152
  Electronic Edition (link) BibTeX
• Tobias Schüle, Klaus Schneider:
  Exact Runtime Analysis Using Automata-Based Symbolic Simulation. 153-162
  Electronic Edition (link) BibTeX
• Jinfeng Huang, Jeroen Voeten, Marc Geilen:
  Real-time Property Preservation in Approximations of Timed Systems. 163-171
  Electronic Edition (link) BibTeX
• Sérgio M. M. Fernandes, Paulo Romero Martins Maciel:
  Reliability Evaluation for Dependable Embedded System Specifications: An Approach Based on DSPN. 172-
  Electronic Edition (link) BibTeX

Invited Talk

• Manfred Broy:
  Modular Hierarchies of Models for Embedded Systems. 183-
  Electronic Edition (link) BibTeX

Refinement II

• Rohit Jindal, Kshitiz Jain:
  Verification of Transaction-Level SystemC models using RTL Testbenches. 199-203
  Electronic Edition (link) BibTeX
• Pierre Wodey, Geoffrey Camarroque, Fabrice Baray, Richard Hersemeule, Jean-Philippe Cousin:
  LOTOS Code Generation for Model Checking of STBus Based SoC: the STBus interconnect. 204-
  Electronic Edition (link) BibTeX

Synthesis, Optimization

• Roberto Ziller, Klaus Schneider:
  A Generalised Approach to Supervisor Synthesis. 217-226
  Electronic Edition (link) BibTeX
• Dumitru Potop-Butucaru, Robert de Simone:
  Optimizations for Faster Execution of Esterel Programs. 227-236
  Electronic Edition (link) BibTeX
• William B. Gardner:
  Bridging CSP and C++ with Selective Formalism and Executable Specifications. 237-
  Electronic Edition (link) BibTeX

Invited Talk

• Arvind:
  Bluespec: A language for hardware design, simulation, synthesis and verification Invited Talk. 249-
  Electronic Edition (link) BibTeX

Formal Verification II

• Christoph Sprenger, Krzysztof Worytkiewicz:
  A Verification Methodology for Infinite-State Message Passing Systems. 255-264
  Electronic Edition (link) BibTeX
• David Cachera, Katell Morin-Allory:
  Verification of Control Properties in the Polyhedral Model. 265-
  Electronic Edition (link) BibTeX

Panel II

• Rajesh K. Gupta, Sandeep K. Shukla:
  Should the space of implementation possibilities be determined by the abilities of high-level synthesis and validation? 277-
  Electronic Edition (link) BibTeX

Closing Talk

• Giovanni De Micheli:
  Robust System Design with Uncertain Information. 283-
  Electronic Edition (link) BibTeX