The goal of the MEMOCODE conference series, the seventh in a series of successful international conferences, is to gather together researchers and practitioners in the field of the design of modern hardware and software systems to explore ways in which future design methods can benefit from new results on formal methods.

Call for papers

Call for papers (pdf)

Camera-ready Author Instructions

Design contest

Conference Program

Conference Location

Conference Registration

Early registration ends 6/15/09

Hotels Information








Invited Speakers:

Amir Pnueli - NYU - Property Synthesis

David Harel - Weizmann - Systems Biology

Martin Rinard - Static Resource Bounds

We have a very interesting tutorial with a great expert:

Thomas Popp from Graz University of Technology will speak about (and show!): implementation attacks & countermeasures

Panel Discussion:

Satnam Singh, Microsoft Research, Cambridge

Klaus Schneider, University of Kaiserslautern

Karen Pieper

Rainer Doemer, University of California, Irvine

Arvind, MIT

Gael Clave, Texas Instruments, Nice

Michael Kishinevsky, Intel



Seventh ACM-IEEE

International Conference on

Formal Methods and Models for Codesign (MEMOCODE'2009)


Stata Center - Room 32-155

  July 13-15, 2009, Cambridge, Massachusetts - USA


General Chairs

Rajesh Gupta (UCSD)
James Hoe (CMU)

Program Chairs

Patrick Schaumont  (Virginia Tech)
Roderick Bloem (Graz U of

Program Committee

Clark Barrett (NYU)
Twan Basten (Eindhoven)
Tevfik Bultan (UCSB)
Luca Carloni (Columbia)
Rainer Doemer (UCI)
Robert de Simone (INRIA)
Rolf Drechsler (Bremen)
Stephen A. Edwards (Columbia)
Franco Fummi (Verona)
David Hwang (GMU)
Ganesh Gopalakrishnan (Utah)
Barbara Jobstmann (EPFL)
Daniel Kroening (Oxford)
Luciano Lavagno (Torino)
Elizabeth Leonard (NRL)
John O'Leary (Intel)
Klaus Schneider (Kaiserslautern)
Satnam Singh (Microsoft)
Frank Vahid (UCR)
Kazutoshi Wakabayashi (NEC)
Reinhard Wilhelm (Saarbruecken)
Fei Xie (Portland State)

Design Contest Chairs

James Hoe (CMU)
Forrest Brewer (UCSB)

Local Chair

Sally Lee (MIT)
Arvind (MIT)


memocode logo

Accepted Papers

Anita Lungu, Pradip Bose, Daniel Sorin, Steven German and Geert Janssen.   
Multicore Power Management: Ensuring Robustness  via Early-Stage Formal   Verification  

Omid Sarbishei, Mahmoud Tabandeh, Bijan Alizadeh and Masahiro Fujita.
High-Level Optimization of Integer Multipliers over a Finite Bit-Width with Verification Capabilities

Daniel Williams, Aprotim Sanyal, Dan Upton, Jason Mars, Sudeep Ghosh and Kim Hazelwood. A Cross-Layer Approach to Heterogeneity and Reliability

Jeannet Bertrand and Briand Xavier.
Combining control and data abstraction in the verification of hybrid systems

Jeong-Han Yun, Chul-Joo Kim, Sunae Seo, Taisook Han and Kwang-Moo Choe. Refining Schizophrenia via Graph Reachability in Esterel

Marco Bozzano, Alessandro Cimatti, Marco Roveri, Joost-Pieter Katoen, Viet Yen Nguyen and Thomas Noll.
Codesign of Dependable Systems: A Component-Based Approach

Fabrizio Ferrandi, Marco Lattuada, Christian Pilato and Antonino Tumeo. Performance Estimation for Task Graphs Combining Sequential Path Profiling and Control Dependence Regions

Malay Ganai and Weihong Li.
Bang for the Buck: Improvising and Scheduling Verification Engines for Effective Resource Utilization

Jens Brandt and Klaus Schneider. Static Data-Flow Analysis of Synchronous Programs

Nalini Vasudevan and Stephen A. Edwards. Buffer Sharing in CSP-like Programs

Eric Chung and James Hoe. Real World Microprocessor Design Using High-level Approaches

Hubert Garavel, Claude Helmstetter, Olivier Ponsini and Wendelin Serwe.
Verification of an Industrial SystemC/TLM Model using Lotos and CADP

Luigi Di Guglielmo, Franco Fummi and Graziano Pravadelli.
The Role of Mutation Analysis for Property Qualification

Peter Boehm. Incremental Modelling and Verification of the PCI Express Transaction Layer

Muralidaran Vijayaraghavan and Arvind Arvind. Bounded Dataflow Networks and Latency-Insensitive Circuits