home Home
venue Venue and Travel
venue Accommodation
program Program
social Social Events
poster Poster
registration Registration
speakers Invited Speakers
venue Accepted Papers
submit Design Contest
cfp Call for Papers

Eighth ACM/IEEE International Conference on
Formal Methods and Models for Codesign

Grenoble, France
July 26-28, 2010

Memocode 2010 was great!
Thanks a lot to all the sponsors, reviewers, panelists, speakers, and attendees.

Pictures from Memocode 2010

Invited Speakers

Jordi Cortadella, Professor at the Universitat Politecnica de Catalunya, Barcelona, Spain

Rupak Majumdar, Professor at University of California, Los Angeles and Scientific Director at MPI for Software Systems, Germany

Eric Flamand, Head of Computing Division at STMicroelectronics, Grenoble, France

Alain Darte, CNRS Research Director, Laboratoire de l'Informatique du Parallelisme, Lyon, France

Josef Haid, Senior Concept Engineer at Infineon Technologies, Graz, Austria

Jordi Cortadella, Professor at the Universitat Politecnica de Catalunya, Barcelona, Spain

Title: Elastic Circuits

Abstract:

Elastic circuits provide tolerance to the variations in computation and communication delays. The incorporation of elasticity opens new opportunities for optimization using new correct-by-construction transformations that cannot be applied to rigid non-elastic circuits. The basics of synchronous and asynchronous elastic circuits will be reviewed. A set of behavior-preserving transformations will be presented: retiming, recycling, early evaluation, variable-latency units and speculative execution. The application of these transformations for performance and power optimization will be discussed. Finally, a novel framework for microarchitectural exploration will be introduced, showing that the optimal pipelining of a circuit can be automatically obtained by using the previous transformations.

Short Biography:

Jordi Cortadella is a full professor at the Department of Software of the Universitat Politecnica de Catalunya (Barcelona, Spain). He obtained his Ph.D. in Computer Science in 1987, at the same University. In 1988, he was a Visiting Scholar at the University of California, Berkeley. He has also been a visiting professor in Intel Corporation (Hillsboro, USA) in summer 1998 and summer 2001 and in Theseus Logic (Sunnyvale, USA) in summer 2000. He co-founded Elastix Corporation in 2007, a company producing EDA tools for asynchronous design.His main research interests include formal methods and computer-aided design of VLSI systems, with special emphasis on asynchronous circuits. He has co-authored over 150 papers in technical journals and conferences. He has served in the technical programme committee of numerous conferences in the area of computer-aided design of VLSI systems and concurrency.

Rupak Majumdar, Professor at University of California, Los Angeles and Scientific Director at Max Planck Institute for Software Systems, Germany

Title: Systematic Testing for Control Applications

Abstract

Software controllers for physical processes are at the core of many safety-critical systems such as avionics, automotive engine control, and process control. Despite their importance, the design and implementation of software controllers remains an art form; dependability is generally poor, and the cost of verifying systems is prohibitive. One problem is the dearth of programmer productivity tools which effectively capture domain constraints.

We show how recent advances in static and dynamic program analyses can be used to cost-effectively verify control system implementations and to bridge the gap between the mathematics of control and the pragmatics of software. In particular, we describe the implementation of the Splat test generation tool for control software and some case studies using Splat.

Short Biography:

Rupak Majumdar received the B.Tech. degree in Computer Science from the Indian Institute of Technology at Kanpur in 1998 and the Ph.D. degree in Computer Science from the University of California at Berkeley in 2003. Since 2003, he has been an Assistant Professor (2003-2008) and an Associate Professor (2008-present) in the Department of Computer Science at the University of California, Los Angeles, and a Scientific Director at the Max Planck Institute for Software Systems (2010). His research interests are in the verification and control of reactive, real-time, hybrid, and probabilistic systems, software verification and programming languages, game theoretic problems in verification, logic, and automata theory. Dr. Majumdar received the President's Gold Medal from IIT, Kanpur, the Leon O. Chua award from UC Berkeley, an NSF CAREER award, and a Sloan Foundation Fellowship.

Eric Flamand, Head of Computing Division at STMicroelectronics, Grenoble, France

Title: The many-cores opportunity for consumer System On Chip.

Abstract:

When looking at some of the fundamental dimensions of Consumer System On Chips like area, power, budget for sub systems, ... it appears that they are quite stable from one generation to another one. In the meanwhile each new technological process node comes with the usual gain predicted by the Moore law. Things that were feasible from a technical view point but not viable from a cost perspective suddenly become affordable. We are currently experimenting this abrupt change for complex sub systems like multimedia, base band, ... where mix of flexible and programmable solutions, many-core like, are becoming realistic. On top of the usual constraints new ones are coming with advanced manufacturing processes. In this talk we will elaborate on this trend and on the challenges they pose both from technical point of view at hardware and software level and from product point of view.

Short Biography:

Currently Director of Advanced Computing with ST Microelectronics Eric Flamand started his career with CNET, the former French Research Center for Telecommunications. He then held various positions both in the academic world and in the industrial world, working on high level synthesis, computer architecture, compilation and operating systems. In his current activities he is working on new classes of programmable architectures that can fully exploit the potential of deep submicron manufacturing technologies.

Alain Darte, CNRS Research Director, Laboratoire de l'Informatique du Parallelisme, Lyon, France

Title: Understanding loops: the influence of the decomposition of Karp, Miller, and Winograd.

Abstract:

Loops are a fundamental control structure in programming languages. Being able to analyze, to transform, to optimize loops is a key feature for compilers to handle repetitive schemes with a complexity proportional to the program size and not to the number of operations it describes. This is true for the generation of optimized sofware as well as for the generation of hardware, for both sequential and parallel execution. The goal of this talk is to recall one of the most important theory to understand loops -- the decomposition of Karp, Miller, and Winograd (1967) for systems of uniform recurrence equations -- and its connections with two different developments on loops: the theory of transformation and parallelization of (nested) DO loops and the theory of ranking functions for proving the termination of (imperative) programs with WHILE loops. Other connections, which will not be covered, include reachability problems in vector addition systems and Petri nets.

Short Biography:

Alain Darte is a research scientist with the French National Council for Scientific Research (CNRS), head of the Inria team Compsys. His education includes an ``Agregation de Mathematiques'' in 1992 and Ph.D. degree in computer science in 1993 from the Ecole normale superieure de Lyon, France. His main scientific interests are in mathematical tools, automatic program transformations, and optimizations for parallelizing compilers and compiler-based tools used to automatically synthesize hardware accelerators. His main contributions include the development of a theory of loop transformations, the use of lattices for scheduling and mapping techniques, and the interest of static single assignment for register allocation.

Josef Haid, Senior Concept Engineer at Infineon Technologies, Graz, Austria

Title: Formal Verification Methods in Low Power Design Flows

Abstract:

The algorithms developed for optimizing the power consumption of integrated circuits are getting increasingly complex. Formal methods are required to verify the correctness of the optimized circuits. The objective of the tutorial is to give a comprehensive overview of recent power optimization techniques proposed in the literature and in commercial tools. Based on the characteristics of the algorithms the tutorial discusses the corresponding formal methods needed to ensure the correctness of the applied algorithms. The tutorial also presents several use-cases from industry, e.g. experiences from the design of RF-powered System-on-chips. Finally the tutorial presents the power emulation methodology that is targeting system-level hardware/software power optimization. The tutorial presents an automated flow and again challenges the algorithms regarding their requirements for formal methods. This tutorial targets VLSI concept engineers, design engineers, researchers and students working in the area of low-power SoC design and all those who are interested in this topic.

Short Biography:

Josef Haid was born 1976 in Linz/Austria. He received a Master's degree in Telematics and a doctoral degree in electrical engineering both from the Technical University of Graz in Austria in the years 2001 and 2003 respectively. Presently he is a senior concept engineer at Infineon Technologies in Graz/Austria and is responsible for development and specification of low power contactless smart cards. His interests include advanced digital design and low power design of hardware and software.
Back