The Coq mailing list

[Klaus.Schneider AT informatik.uni-kl.de]

                           -- CALL FOR PARTICIPATION --

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

                September 29 - October 2, 2017, Vienna, Austria
                         http://memocode.irisa.fr/2017

                                co-located with

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

REGISTRATION:
    http://memocode.irisa.fr/2017/registration.html
    
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 Jääskeläinen, Hannu-Matti Järvinen 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