MEMOCODE 2017

15th ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)

co-located withInternational Conference on Formal Methods in Computer-Aided Design (FMCAD)
http://www.fmcad.org/FMCAD17

MEMOCODE's objective is to bring together researchers and practitioners interested in formal methods and models for system design and development to exchange ideas, research results, and lessons learned. System design covers the development of hardware, firmware, middleware, and application software for systems ranging from single embedded devices to highly networked CPS and systems in the IoT. In particular, MEMOCODE 2017 seeks research contributions on formal foundations, engineering methods, tools, and experimental case studies. Research areas of interest include, but are not limited to the following:

Modeling Languages, Methods and Tools:

• Programming languages and models; software and system modeling languages;
• architecture and high-level hardware description languages; timing models;
• model and program synthesis methods; model transformation methods

Formal Methods and Tools:

• Correct-by-construction methods; contract-based design and verification;
• static, dynamic, and type theoretic analysis; verification; validation;
• probabilistic model checking; test generation; refinement-based and
• compositional approaches to design and verification

Models and Methods for Developing Critical Systems:

• Fault-tolerant systems; security-critical and safety-critical systems;
• cyber-physical systems; hybrid systems; autonomous systems;
• self-adapting systems

Quantitative/Qualitative Reasoning:

• Power/performance/cost/latency estimation methods;
• system models for quantitative design space exploration

Formal Methods/Models in Practice:

• Design case studies; empirical case studies

KEYNOTES

• Alessandro Abate, University of Oxford:
  Formal Verification and Control Synthesys of Complex Dynamic Systems: Model-Based and Data-Driven Methods
• Franz-Josef Grosch, Robert Bosch GmbH:
  Elevate embedded real-time programming with a synchronous language.
• Thomas Henzinger, IST Austria:
  The Quest for Average Response Time

TUTORIALS (shared with FMCAD)

• Jade Alglave, University College London / Microsoft Research:
  Consistency properties of parallel/distributed programs in cat
• Cas Cremers, Oxford University:
  Symbolic Security Analysis using the Tamarin Prover
• Shin'ichiro Matsuo (MIT Media Lab/CELLOS Consortium/BSafe.network):
  How Formal Methods and Analysis Helps Security of Entire Blockchain-based Systems

ACCEPTED PAPERS

• Antti Jaaskelainen, Hannu-Matti Jarvinen and Mikko Tiusanen.
  Concurrent Execution System for Action Languages
• Kenneth Roe and Scott Smith.
  Using the Coq theorem prover to verify complex data structure invariants
• Assaf Marron.
  A Reactive Specification Formalism for Enhancing System Development, Analysis and Adaptivity
• Guillaume Plassan, Katell Morin-Allory and Dominique Borrione.
  Extraction of Missing Formal Assumptions in Under-Constrained Designs
• Jiwei Li, Pierluigi Nuzzo, Alberto Sangiovanni-Vincentelli, Yugeng Xi and Dewei Li.
  Stochastic Contracts for Cyber-Physical System Design Under Probabilistic Requirements
• Thomas Reynolds, Adam Procter, William Harrison and Gerard Allwein.
  A Core Calculus for Secure Hardware: Its Formal Semantics and Proof System
• Hammond Pearce, Matthew Kuo, Nathan Allen, Partha Roop and Avinash Malik.
  Simulation of Cyber-physical systems using IEC61499
• Stephen A. Edwards, Richard Townsend and Martha A. Kim.
  Compositional Dataflow Circuits
• Arun Chandrasekharan, Daniel Grosse and Rolf Drechsler.
  Yise - A novel Framework for Boolean Networks using Y-Inverter Graphs
• Ezio Bartocci, Luca Bortolussi, Michele Loreti and Laura Nenzi.
  Monitoring Mobile and Spatially Distributed Cyber-Physical Systems
• Haven Skinner, Rafael Possignolo and Jose Renau. Liam:
  An Elastic Programming Model
• Sudipta Chattopadhyay, Moritz Beck, Ahmed Rezine and Andreas Zeller.
  Quantifying the Information Leak in Cache Attacks via Symbolic Execution
• Hsin-Hung Lin and Bow-Yaw Wang.
  Releasing VDM Proof Obligations with SMT Solvers
• Jakob Mund, Maximilian Junker, Safa Bougouffa, Suhyun Cha and Birgit Vogel-Heuser.
  Model-Based Availability Analysis for Automated Production Systems: A Case Study
• Jean-Paul Bodeveix, Mamoun Filali-Amine and Kan Shuanglong.
  A Refinement-based compiler development for synchronous languages
• Andreas Fellner, Willibald Krenn, Thorsten Tarrach, Georg Weissenbacher and Rupert Schlick.
  Model-based, mutation-driven test case generation via heuristic-guided branching search
• Stefan Resmerita, Andreas Naderlinger and Stefan Lukesch.
  Efficient Realization of Logical Execution Times in Legacy Embedded Software
• Max Scheerer, Axel Busch and Anne Koziolek.
  Automatic Evaluation of Complex Design Decisions in Component-based Software Architectures
• Elizabeth Leonard, Myla Archer and Constance Heitmeyer.
  Property Templates for Checking Source Code Security
• Nils Przigoda, Philipp Niemann, Judith Peters, Frank Hilken, Robert Wille and Rolf Drechsler.
  More than true or false: Native Support of Irregular Values in the Automatic Validation & Verification of UML/OCL Models
• Tim Gonschorek, Frank Ortmeier, Ben Lukas Rabeler and Dirk Schomburg.
  On Improving Rare Event Simulation for Probabilistic Safety Analysis
• Luan Nguyen, James Kapinski, Xiaoqing Jin, Jyotirmoy Deshmukh and Taylor T Johnson.
  Hyperproperties of Real-Valued Signals

PROGRAM CHAIRS

• Patricia Derler, National Instruments Corporation
• Klaus Schneider, University of Kaiserslautern

GENERAL CHAIR

• Jean-Pierre Talpin, IRISA

PUBLICATION CHAIR

• Yi Deng, Virginia Tech

PROGRAM COMMITTEE

• Paul Attie, American University of Beirut
• Marco Bekooij, University of Twente
• Jani Boutellier, Tampere University of Technology
• Jens Brandt, Hochschule Niederrhein
• Sudipta Chattopadhyay, Singapore University of Technology and Design
• Silviu Craciunas, TTTech Computertechnik AG
• Jyotirmoy Deshmukh, Toyota Technical Center
• Stephen Edwards, Columbia University
• Mamoun Filali-Amine, IRIT
• Martin Fraenzle, Carl von Ossietzky Universitaet Oldenburg
• Franco Fummi, University of Verona
• Abdoulaye Gamatie, CNRS
• Marc Geilen, Eindhoven University of Technology
• Leonard Gerard, ENS
• Gregor Goessler, INRIA
• Tuba Kahveci, University of Florida
• Rick Kuhn, Natl Institute of Standards & Technology
• Luciano Lavagno, Politecnico di Torino
• Axel Legay, IRISA/INRIA, Rennes
• Elizabeth Leonard, Naval Research Laboratory
• Thanhvu Nguyen, University of Nebraska, Lincoln
• Pierluigi Nuzzo, University of Southern California
• John O'Leary, Intel Corporation
• Roberto Passerone, University of Trento
• Maxime Pelcat, IETR/INSA
• Doron Peled, Bar Ilan University
• Andre Platzer, Carnegie Mellon University
• Murali Rangarajan, The Boeing Company
• Sanjai Rayadurgam, University of Minnesota
• Elvinia Riccobene, University of Milan
• Partha Roop, University of Auckland
• Neda Saeedloei, University of Texas at Dallas
• Aviral Shrivastava, Arizona State University
• Sandeep Shukla, IIT Kanpur
• Marjan Sirjani, Reykjavik University
• Juergen Teich, University of Erlangen-Nuremberg
• Stavros Tripakis, University of California, Berkeley
• Muralidaran Vijayaraghavan, MIT
• Reinhard von Hanxleden, Christian-Albrechts-Universitaet zu Kiel
• Qi Zhu, UC Riverside
• Damian Zufferey, MPI Software Systems