Day 1: Monday September 21, 2015




General Chair: Andreas Gerstlauer (U. Texas, Austin)
Program Co-Chairs: Elizabeth Leonard and Constance Heitmeyer (NRL)



Keynote 1 (Chair: Angelo Gargantini)


Rajeev Alur (University of Pennsylvania)
Syntax-Guided Synthesis



Coffee Break



Session 1: Distributed Systems and Concurrency (Chair: Stephen Edwards)


Alon Brook, Doron Peled and Sven Schewe.
Local and Global Fairness in Concurrent Systems

Karsten Rathlev, Steven Smyth, Christian Motika, Reinhard Von Hanxleden and Michael Mendler.
SCEst: Sequentially Constructive Esterel

Wenchao Li, Leonard Gerard and Natarajan Shankar.
Design and Verification of Multi-Rate Distributed Systems



Short Paper Session 1


Ahlem Triki, Jacques Combaz and Saddek Bensalem.
Optimized Distributed Implementation of Timed Component-based Systems

Jean-Pierre Talpin, Pierre Jouvelot and Sandeep Kumar Shukla.
Towards Refinement Types for Time-Dependent Data-Flow Networks

Alan Leung, Dimitar Bounov and Sorin Lerner.
C-To-Verilog Translation Validation






Design Contest Presentation (Chair: Peter Milder)


Peter Milder

MEMOCODE 2015 Design Contest: Continuous Skyline Computation

First Place: Kenichi Koizumi, Mary Inaba, Kei Hiraki, University of Tokyo

Efficient Implementation of Continuous Skyline Computation on a Multi-Core Processor

Second Place: Armin Ahmadzadeh, Ehsan Montahaie, Milad Ghafouri, Reza Mirzaei, Saied Rahmani, Farzad Sharif Bakhtiar, Mohsen Gavahi, Rashid Zamanshoar, Hanie Ghasemi, Kianoush Jafari, Saeid Gorgin, Inst. for Research in Fundamental Sciences (IPM), Iran

Efficient Continuous Skyline Computation on Multi-Core Processors Based on Manhattan Distance



Coffee Break



Panel: Formal Methods: How Can We Increase Usage in Practice? (Organizer and Chair: Sandeep Shukla)





Welcome Reception


Day 2: Tuesday September 22, 2015


Keynote 2 (Chair: Andreas Gerstlauer)


Derek Chiou (U. Texas, Austin and Microsoft Research)
Accelerating Data Centers using Reconfigurable Logic



Coffee Break



Session 2: System and Software Modeling and Verfication (Chair: Jean-Pierre Talpin)


Abdur Rakib and Hafiz Mahfooz Ul Haque.
Modeling and verifying context-aware non-monotonic reasoning agents

Adel Dokhanchi, Bardh Hoxha and Georgios Fainekos.
Metric Interval Temporal Logic Specification Elicitation and Debugging

Paolo Arcaini, Silvia Bonfanti, Angelo Gargantini, Atif Mashkoor and Elvinia Riccobene.
Formal Validation and Verification of a Medical Software Critical Component



Short Paper Session 2


Michael W. Whalen, Sanjai Rayadurgam, Elaheh Ghassabani, Anitha Murugesan, Oleg Sokolsky, Mats P.E. Heimdahl and Insup Lee.
Hierarchical Multi-Formalism Proofs of Cyber-Physical Systems

Joao Bastos, Sander Stuijk, Jeroen Voeten, Ramon Schiffelers, Johan Jacobs and Henk Corporaal.
Modeling Resource Sharing using FSM-SADF

Masahiro Fujita.
Logic analysis and optimization with quick identification of invariants through one time frame analysis






Session 3: Hardware Design and Test (Chair: Masahiro Fujita)

David Greaves.
Layering RTL, SAFL, Handel-C and Bluespec Constructs on Chisel HCL

Jonathan Beaumont, Andrey Mokhov, Danil Sokolov and Alex Yakovlev.
Compositional design of asynchronous circuits from behavioural concepts

Matthew Naylor and Simon Moore.
A Generic Synthesisable Test Bench



Coffee Break



Session 4: System and Software Testing, Repair, and Deployment (Chair: Doron Peled)


William Durand and Sebastien Salva.
Passive testing of production systems based on model inference

Paul Attie, Ali Cherri, Kinan Dak Al Bab, Mouhammad Sakr and Jad Saklawi.
Model and Program Repair via SAT Solving

Stefan Kugele, Gheorghe Pucea, Ramona Popa, Laurent Dieudonne and Horst Eckardt.
On the Deployment Problem of Embedded Systems



Bus departs for Conference Dinner


Conference Banquet at Lamberts Downtown Barbecue


Bus returns


Day 3: Wednesday September 23, 2015


Keynote 3 (Chair: Elizabeth Leonard)


Paul Clements (BigLever Software)
A Formal Methods Perspective on Product Line Engineering



Coffee Break



Session 5: Hardware and Architecture Design and Analysis (Chair: David Greaves)


Jan Lanik, Julien Legriel, Erwan Piriou, Emmanuel Viaud, Fahim Rahim, Oded Maler and Solaiman Rahim.
Reducing Power with Activity Trigger Analysis

Bingyi Cao, Kenneth A. Ross, Martha A. Kim and Stephen A. Edwards.
Implementing Latency-Insensitive Dataflow Blocks

Alexandru Tanase, Michael Witterauf, Juergen Teich and Frank Hannig.
Symbolic Loop Parallelization for Balancing I/O and Memory Accesses on Processor Arrays

Sanne Wouda, Sebastiaan J. C. Joosten and Julien Schmaltz.
Process algebra semantics & reachability analysis for micro-architectural models of communication fabrics






Session 6: Runtime Verification (Chair: Klaus Schneider)


Martial Chabot, Kevin Mazet, and Laurence Pierre.

Automatic and Configurable Instrumentation of C Programs with Temporal Assertion Checkers

Stefan Jaksic, Ezio Bartocci, Radu Grosu, Reinhard Kloibhofer, Thang Nguyen and Dejan Nickovic.

From Signal Temporal Logic to FPGA Monitors






Session 7: Hybrid Systems Verification (Chair: Elvinia Riccobene)


Pierre Ganty, Samir Genaim, Ratan Lal and Pavithra Prabhakar.

From Non-Zenoness Verification to Termination

Xian Li and Klaus Schneider.

Verification Condition Generation for Hybrid Systems

Daniel Ricketts, Gregory Malecha, Mario M. Alvarez, Vignesh Gowda and Sorin Lerner.

Towards Verification of Hybrid Systems in a Foundational Proof Assistant