First ACM & IEEE International Conference on

Formal Methods and Models for Codesign (MEMOCODE'2003)

Programming models, formal analysis methods and verification techniques for high-level
system design and (re)engineering: towards convergence of formal methods and industrial trends.

June 24th.-26th., 2003 -- Mont Saint-Michel, France



Opening speaker
Jose Meseguer (UIUC)

Invited speakers
Arvind (MIT)
Manfred Broy (TUM)
Giovanni De Micheli (Stanford)
Ken McMillan (Cadence)

Aims and scope

Call for papers

High-level models and languages
Analysis and verification
Methodological issues
Reuse and component-based design
Distribution: fault-tolerance, scheduling
Non-functional requirements
Industrial case studies

Conformance checking
Hierarchical verification
Abstraction vs. optimization
Incremental verification
Post-production patchability

Final program


The MEMOCODE'2003 proceedings are now available online from the IEEE.

Selected papers from the conference will be published in a special issue of the ACM TECS (see call for papers) and in a special volume by Kluwer Academic Publishers on a later date.


Sponsorship

IEEE Circuits and System Society
ACM Special Interest Group on Digital Automation
IEEE Computer Society, Digital Automation Technical Committee

Organized at the Relais du Mont Saint-Michel
in cooperation with INRIA and IRISA.



High-level design and modeling of hardware and embedded hardware-software systems has gained prominence in the face of rising technological complexities and performances, as well as shortened time to market demands for complex electronic equipments. Numerous programming languages, tools and frameworks have been proposed in the past to design, simulate and validate heterogeneous systems within an abstract and rigorously defined mathematical model. Recently, attention has shifted to modeling frameworks based on variants of general purpose programming languages, in response to the growing industry demand for use of higher levels of abstraction in the system design process. Meanwhile, the installed base of existing IP adds further requirements for the adaptation of existing IPs with new services within complex integrated architectures, calling for appropriate methodological approaches.

Whereas abstract frameworks are ways to unambiguously model the essense of hardware software systems, help understand the design, implement formal correctness proofs, predict performances and other metrics; general-purpose languages facilitate programming, reuse and gain from the popularity of C, C++ like languages. Still, important gaps need to be filled and bridges to be built between the theory of modelizing and the practice of programming. Languages shall benefit the rigorousness of models and models the experience of programming practice. This calls for finding a convergence between both approaches. A focus on formal methods (programming and concurrency models, analysis and verification techniques) for hardware/software codesign is necessary, because language in which system designers work are general-purpose ones, because the only way provably correct systems can be constructed are by technology transfer of research in formal methods.

Donators : INRIA, University of Rennes 1, CNRS.