MEMOCODE 2004

CALL FOR PAPERS Common trends and common problems have emerged lately in the hardware and software industries. In the hardware industry, the growing complexity of hardware components (e.g., systems-on-chip), the challenge of design verification, and the need to meet the competing objectives of performance/power/time-to-market have made it essential to increase the level of abstraction in the hardware design process. The response has been increased use of high-level modeling, using variants of traditional hardware description languages (System Verilog) or general-purpose programming languages (SystemC, SpecC). Similar pressures exist in the software industry: the increasing complexity of software systems coupled with the need for increased performance and lower cost have led important sectors of the industry, e.g., avionics companies, to adopt model-based approaches to software development and to increase usage of modeling languages such as UML. In both software and hardware, the availability of standard IP components has produced an urgent need for new methods to adapt and integrate these components to build reliable, cost-effective systems. The abstract models, languages, and analysis techniques produced by formal methods research provide a sound methodological basis for the high-level modeling, design, and development of both hardware and software and for adapting and integrating existing components to meet new requirements.
The goal of MEMOCODE 2005, the third in a series of international conferences, is to gather together software and hardware researchers and practitioners to explore ways in which software and hardware design can exploit research results in formal methods. Papers, panel proposals, and tutorial proposals are invited on topics relevant to the application of formal methods to hardware and software design. These topics include formal specification languages and their use in modeling hardware and software systems, formal methods for performance/power analysis and optimization, design verification approaches using model checking and theorem proving, specification-based testing, design methodologies based on formal methods, and rigorous approaches (e.g., refinement) to transforming a hardware or software specification into a reliable, efficient implementation.

NEW TO MEMOCODE 2005 One new feature is a special panel session organized by Manfred Broy to discuss the role of formal methods and co-design in the automobile industry. This session will focus on current problems, hot topics (such as model-based design), and trends in hardware design and software development in the automotive sector. A second new feature, inspired by D.A. Patterson’s Dec. 2004 CACM article on “The Health of Research Conferences and the Dearth of Big Idea Papers,” is a special technical session of papers which present either big ideas or new directions in formal methods. More details about the special session will be available soon.