Visible to the public Call for Participation: MEMOCODE 2017Conflict Detection Enabled

No replies
Anonymous's picture


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

September 29 - October 2, 2017 | Vienna, Austria |

co-located withInternational Conference on Formal Methods in Computer-Aided Design (FMCAD)



  • 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/
    How Formal Methods and Analysis Helps Security of Entire Blockchain-based Systems


  • 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