ACM-IEEE MEMOCODE'14

The 12th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE'14) will be held at EPFL in Lausanne, Switzerland on October 19-21, 2014. MEMOCODE'14 will be collocated with FMCAD'14, the 14th Conference on Formal Methods in Computer-Aided Design, providing attendees the opportunity to attend joint tutorial sessions and keynotes. The joint MEMOCODE'14 and FMCAD'14 tutorials will be held on October 21st.

Keynotes

Joseph Sifakis,
Turing Award

EPFL

System Design - Challenges and Work Directions
Modern computing systems break with traditional systems, such as desktop computers and servers, in various ways: 1) they are instrumented in order to interact with physical environments; 2) they are interconnected to allow interaction between people and objects in entirely new modes; 3) they must be smart to ensure predictability of events and optimal use of resources. Currently, we lack theory methods and tools for building cost-effectively trustworthy systems.
In this talk, I will discuss system design as a formal and accountable process leading from requirements to correct-by-construction implementations. I will also discuss current limitations of the state of the art and advocate a coherent scientific foundation for system design by presenting a vision raising three grand challenges: 1) linking the cyber and the physical worlds; 2) correct component-based construction; 3) intelligence.
I will conclude with general remarks about the nature of computing and advocate a deeper interaction and cross-fertilization with other more mature scientific disciplines.

Wayne Burleson
University of Massachusetts at Amherst

Security and privacy in implantable medical devices: an ongoing concern
In the last 5 years, there has been a considerable increase in research and awareness of security and privacy issues in implantable medical devices. This has been driven by the rapid introduction and deployment of an increasing diversity of medical devices. Although wearable and clinical devices are also of interest, the implantable nature of many recent devices significantly increases risks as well as engineering challenges. This talk will use several case studies to review the multi-disciplinary process in which vulnerabilities are analyzed, disclosed, and repaired. Business incentives and regulations play an important role in the overall process.
Technical challenges include energy harvesting, side-channel protection, lightweight crypto, personalization, wireless communications, security/safety tradeoffs, and human factors. Several open research areas will be discussed.

Bertrand Meyer
ETH Zurich and Eiffel Software

Proving (and revisiting) what programs do not
In 2007, I had the honor of an invited presentation at MEMOCODE, where I discussed the frame problem: how to establish that programs do *not* modify certain properties. The problem is particularly challenging in the case of object-oriented programs involving complex pointer (reference) data structures. Seven years later, it is still largely an open problem, although significant progress has occurred. After realizing that a satisfactory solution requires addressing another difficult problem, alias analysis, I have devoted much of my work to program analysis techniques that tackle both aliasing and framing. Taking advantage of the kind invitation to present again at MEMOCODE, I will describe the current state of this work and how its results are embodied in program analysis tools that provide automatic means -- not requiring program annotations -- to ascertain fundamental properties of programs.

Tutorials

Johannes Kinder
Royal Holloway, University of London

Efficient symbolic execution for software testing
Symbolic execution has proven to be a practical technique for building automated test case generation and bug finding tools. While the basic technique had been introduced already in the 70s, the advent of modern SAT and SMT solvers has lead to a surge of tools and techniques in the area over the last decade. This tutorial will introduce and compare the different approaches to using symbolic execution for testing and discuss the specific challenges and trade-offs. A main challenge in symbolic execution is path explosion, and various proposals have been made to either combat it. I will discuss how these techniques affect the number and type of solver queries that have to be made, and how this can lead to surprising effects on the efficiency of a symbolic execution engine. Going further, we will look at developments to increase the scope of symbolic execution to larger software systems. Specific topics covered include state merging, procedure summaries, abstraction, search strategies, and parallelization.

Armin Biere
Johannes Kepler University, Linz

Challenges in Bit-Precise Reasoning
Bit-precise reasoning (BPR) precisely captures the semantics of systems down to each individual bit and thus is essential to many verification and synthesis tasks for both hardware and software systems. As an instance of Satisfiabiliy Modulo Theories (SMT), BPR is in essence about word-level decision procedures for the theory of bit-vectors. In practice, quantiers and other theory extensions, such as reasoning about arrays, are important too. In the first part of the tutorial we gave a brief overview on basic techniques for bit-precise reasoning and then covered more recent theoretical results, including complexity classification results. We discussed challenges in developing an efficient SMT solver for bit-vectors, like our award winning SMT solver Boolector, and in particular presented examples, for which current techniques fail. Finally, we reviewed the state-of-the-art in word-level model checking, and argued why it is necessary to put more effort in this direction of research.

Program

October 19th, Conference

 

8:30 – 9:00  Coffee and Registration

 

9:00 – 9:10  Introductory Remarks

Giovanni De Micheli, General Chair

Jean-Pierre Talpin, TPC Co-Chair

Sandeep Shukla, TPC Co-Chair

 

9:10 – 10:30  Opening Keynote - Chair: Giovanni De Michelli

Security and privacy in implantable medical devices: an ongoing concern

Wayne Burleson, Univ. of Massachusetts, Amherst

 

10:30 – 11:00 Coffee Break

 

11:00 – 13:00 Session I:  Scheduling - Chair: Paolo Ienne

 

Adnan Bouakaz and Thierry Gautier

An Abstraction-Refinement Framework for Priority-Driven Scheduling of Static Dataflow Graphs

 

Joost Hausmans, Stefan Geuns, Maarten Wiggers and Marco Bekooij

Unified Dataflow Model for the Analysis of Data and Pipeline Parallelism, and Buffer Sizing

 

Michal Karczmarek, Arvind and Muralidaran Vijayaraghavan

A new synthesis procedure for atomic rules containing multi-cycle function blocks

 

Yu Bai, Klaus Schneider, Nikita Bhardwaj, Badarinath Katti and Tania Shazadi

From Clock-Driven to Data-Driven Models (short presentation)

 

Ke Sun, Loic Besnard and Thierry Gautier

Optimized Distribution of Synchronous Programs via a Polychronous Model (short presentation)

 

13:00 – 14:00 Lunch

 

14:00 – 16:00  Session 2: High Assurance Software - Chair: Moshe Vardi

 

Torben Scheffel and Malte Schmitz

Three-Valued Asynchronous Distributed Runtime Verification

 

Prakash Chandrasekaran, Deepak D'Souza, Shibu Kumar Kb, Remish L. Minz and Lomesh Meshram

A Multi-Core Version of FreeRTOS Verified for Datarace and Deadlock Freedom

 

Robin Larrieu and Natarajan Shankar

High-Assurance Quasi-Synchronous Systems

 

Ying Qin and Shengyu Shen

Structure-Aware CNF Obfuscation for Privacy-Preserving SAT Solving (short presentation)

 

 Rubén Trillo and Marc Boyer

Performance analysis of the Disrupted Static Priority scheduling for AFDX (short presentation)

 

 

16:00 –16:30 Coffee Break

 

16:30 – 18:00 Session 3: Models, Components, Contracts and Interfaces - Chair: Klaus Schneider

 

 Pierluigi Nuzzo, Antonio Iannopollo, Stavros Tripakis and Alberto Sangiovanni-Vincentelli

Are Interface Theories Equivalent to Contract Theories?

 

Frédéric Boulanger, Christophe Jacquet, Cecile Hardebolle and Iuliana Prodan

TESL: a Language for Reconciling Heterogeneous Execution Traces

 

 Sam Procter and John Hatcliff.

An Architecturally-Integrated, Systems-Based Hazard Analysis for Medical Applications (short presentation)

 

Thi Thieu Hoa Le and Roberto Passerone

 Refinement-based Synthesis of Correct Contract Model Decompositions (short presentation)

 

18:30 Bus Departure to the Social Swiss Dinner

 

October 20th, Conference

 

8:30  – 10:00 Second Key Note - Chair: Sandeep Shukla 

Proving (and revisiting) what programs do not

Bertrand Meyer,  ETH Zurich

 

10:00 – 10:30 Coffee Break

 

10:30 – 12:30 Session 4: High Assurance Hardware - Chair: Arvind

 

Sonali Dutta and Moshe Vardi

Assertion-Based Flow Monitoring of SystemC Models

 

Houssam Abbas, Georgios Fainekos and Hans Mittelmann

Formal property verification in a conformance testing framework

 

Ranan Fraer, Doron Keren, Zurab Khasidashvili, Alexander Novakovsky, Avi Puder, Eli Singerman, Eran Talmor, Moshe Vardi, Jin Yang

 From Visual to Logical Formalisms for SoC Validation

 

Khaza Anuarul Hoque, Otmane Ait Mohamed, Yvon Savaria and Claude Thibeault

Probabilistic Model Checking Based DAL Analysis to Optimize a Combined TMR-Blind-Scrubbing Mitigation Technique for FPGA-Based Aerospace Applications

 

 

12:30 – 1:30 Lunch

 

1:30  – 3:00   Session 5: MEMOCODE Design & Software Contest

 

Software Contest

 

1st Place

David Richie and James Ross 

Cycle-Accurate 8080 Emulation Using an ARM11 Processor with Dynamic Binary Translation

 

2nd Place

Nariman Eskandari, Hatef Madani, Armin Ahmadzadeh, Mohsen Mahmoudi Aznaveh, and Saeid Gorgin

A Fast Emulator for ARM-based Embedded Systems

 

3rd Place

Pablo González Aledo Marugán, Luis Díaz Suárez, Álvaro Díaz Suárez, Pablo Sánchez

Profiling and optimizations for Embedded Systems

 

 

Co-Design Contest

 

Performance Winner

Kevin Townsend, Phillip Jones, Joseph Zambreno

A High Performance Systolic Architecture for k-NN Classification

 

Cost Adjusted Performance Winner

Armin Ahmadzadeh, Reza Mirzaei, Hatef Madani, Mohammad, Shobeiri, Mahsa Sadeghi, Mohsen Gavahi, Kianoush Jafari, Mohsen, Mahmoudi Aznaveh, Saeid Gorgin

Cost-Efficient Implementation of k-NN Algorithm on Multi-Core Processors

 

 

3:00 – 4:00 Session 6: Many Core - Chair: Jean-Pierre Talpin

 

Ayoub Nouri, Marius Bozga, Anca Molnos, Axel Legay and Saddek Bensalem

Building Faithful High-level Models and Performance Evaluation of Manycore Embedded Systems

 

Alexandru Tanase, Michael Witterauf, Jürgen Teich and Frank Hannig

Symbolic Inner Loop Parallelisation for Massively Parallel Processor Arrays

 

 

4:00 – 4:15 Coffee Break

 

4:15 – 17:30 Final Key Note and EPFL Colloquium - Chair: Rajesh Gupta

System Design - Challenges and Work Directions

Joseph Sifakis, EPFL

 

17:30 Conference Closing Remarks                                                                                        

 

October 21st, Joint Tutorials (MEMOCODE & FMCAD)

Regular presentation are 30mn long including 5mn question time.
Short presentations are 15mn long including 3mn question time.

Registration

Secure online registration is available from at EPFL here .
Please note that the early registration deadline is September 17th, 2014.

Venue

The 12th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE'14) will be held at EPFL in Lausanne, Switzerland on October 19-21, 2014. MEMOCODE'14 will be collocated with the FMCAD'14, the 14th Conference on Formal Methods in Computer-Aided Design.

Location

A short video about Lausanne

Conference location on Google

An interactive map of EPFL

Hotels

Call for Papers

    MEMOCODE'14 provides an excellent venue for researchers working on formal methods and models for embedded hardware and software design (co-design).
    In the past editions, MEMOCODE emphasized co-design as its primary focus, but over the last decade, the clear boundaries between system components implemented in hardware, firmware, software, middleware or applications have blurred. This evolution in system design practices has necessitated a change in the title of the conference to cater to the needs of today's industry and research practices. MEMOCODE's main agenda is to bring together researchers in software design, hardware design, as well as hardware/software co-design, and exchange ideas, research results, lessons learned from each other and apply them to each other's areas. We want to emphasize the importance of models and methodologies in correct system design, and provide a platform for researchers and industry practitioners who work in any or all components of the system stack - hardware, firmware, middleware, software, architecture and applications.
    MEMOCODE'14 seeks research contributions addressing all aspects of methods and models for hardware and embedded software design. We are interested in formal foundations, informal engineering methodologies with sound basis, model driven approaches, design tools, design case studies and industry-scale experimental case-studies. Research areas of interest to MEMOCODE consist of (but not limited to) the following topics:
    • Programming models, languages, methodologies and tools
    • Analysis, verification and test in system design
    • Refinement, component, platform-based design methodologies
    • Models of time in system design, and the relations
    • Fault tolerance, fault models, reliability and resilience
    • Quantitative and qualitative reasoning in system design
    • Cyber-secure and trustworthy system design
    • Case studies and tools paper
    Paper submissions through Easychair are open. Papers must be written in English, formatted following IEEE Computer Society guidelines and not exceed 10 pages. Submissions must describe original work that does not overlap a publication or submission to another journal or conference. Accepted papers will be published as IEEE conference proceedings and included in IEEE-Xplore. Selected papers will be invited for publication in a special section of the ACM Transactions of Embedded Computing Systems.

    Design Contest

      MEMOCODE has a long history of a successful co-design contest section. Even within this design contest, we have seen an evolving trend. Initially the challenge problem started to be implemented as synthesis of co-processors for co-designing a specific computation intensive system. Today, with GPUs, FPGA boards and other flexible hardware add-ons, we often find even software solutions that compete well with the purely co-processor based co-design solutions. This year, we plan to introduce a software tool contest along with our traditional design contest to interest more software developers in taking part in MEMOCODE and showcase their skills in making software tools that instantiate methodologies and model-based approaches to system design.
      As a result, MEMOCODE'14 will entail two design contest tracks, for which additional call for participations will be issued, and a vibrant research track that will seek submissions from researchers and industrial engineers for presentation at the conference main track. The conference will sponsor at least one prize with a monetary award for each contest. Each team delivering a complete and working solution will be invited to prepare a 2-page abstract to be published in the proceedings and to present it during a dedicated poster session at the conference. The winning teams will be invited to contribute a 4-page short paper for presentation in the conference program. Detailed information on the design contest and software contest will be made available on this website by June 1st, 2014.

      Important Dates

      • Abstract submission deadline July 10
      • Paper submission deadline July 17, extended to July 24th, 24:00, NY Time
      • Notification of acceptance August 14, delayed August 19th, 2014
      • Final version of papers September 4
      • Venue October 19-21, 2014

      Organisation

      • General Chair Giovanni De Micheli, EPFL
      • Program Chairs Sandeep Shukla, VT, and Jean-Pierre Talpin, INRIA
      • Design Challenge Chair Peter Milder, Stony Brook
      • Software Challenge Chairs Stephen Edwards, Columbia, and Hiren Patel, Waterloo
      • Publication Chair Deng Yi, VT
      • Local Chair David Atienza, EPFL
      • Finance Chair Paolo Ienne, EPFL

      Program Committee


      • Francois Bodin, IRISA
      • Dominique Borrione, TIMA
      • Manfred Broy, TUM
      • Luca Carloni, Columbia University
      • Nirav Dave, MIT CSAIL
      • Stephen Edwards, Columbia University
      • Hans Eveking, Technische Universitaet Darmstadt
      • Mamoun Filali-Amine, IRIT
      • Masahiro Fujita, University of Tokyo
      • Franco Fummi, University of Verona
      • Harry Foster, Mentor Graphics
      • Abdoulaye Gamatie, LIRMM
      • Thierry Gautier, INRIA
      • Constance Heitmeyer, Naval Research Laboratory
      • Daniel Kroening, University of Oxford
      • Thomas Kuhn, University of Kaiserslautern
      • Luciano Lavagno, Politecnico di Torino
      • Axel Legay, INRIA
      • Elizabeth Leonard, Naval Research Laboratory
      • Frederic Mallet, University of Nice
      • John O'Leary, Intel Corporation
      • Claire Pagetti, ONERA
      • Roberto Passerone, University of Trento
      • Hiren Patel, University of Waterloo
      • Zebo Peng, Linkoeping University
      • Dumitru Potop-Butucaru, INRIA
      • Marly Roncken, Portland State University
      • Klaus Schneider, University of Kaiserslautern
      • Sander Stuijk, Eindhoven University of Technology
      • Michael Theobald, D. E. Shaw Research
      • Fei Xie, Portland State University

      Past Editions

      Sponsors