Day 1: Monday September 21, 2015

08:45	Welcome
	General Chair: Andreas Gerstlauer (U. Texas, Austin) Program Co-Chairs: Elizabeth Leonard and Constance Heitmeyer (NRL)
09:00	Keynote 1 (Chair: Angelo Gargantini)
	Rajeev Alur (University of Pennsylvania) Syntax-Guided Synthesis
10:00	Coffee Break
10:30	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
12:00	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
12:30	Lunch
14:00	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
15:00	Coffee Break
15:30	Panel: Formal Methods: How Can We Increase Usage in Practice? (Organizer and Chair: Sandeep Shukla)
17:00	Welcome Reception

Day 2: Tuesday September 22, 2015

09:00	Keynote 2 (Chair: Andreas Gerstlauer)
	Derek Chiou (U. Texas, Austin and Microsoft Research) Accelerating Data Centers using Reconfigurable Logic
10:00	Coffee Break
10:30	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
12:00	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
12:30	Lunch
14:00	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
15:30	Coffee Break
16:00	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
18:00	Bus departs for Conference Dinner
18:30	Conference Banquet at Lamberts Downtown Barbecue
21:30	Bus returns

Day 3: Wednesday September 23, 2015

09:00	Keynote 3 (Chair: Elizabeth Leonard)
	Paul Clements (BigLever Software) A Formal Methods Perspective on Product Line Engineering
10:00	Coffee Break
10:30	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
12:30	Lunch
14:00	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
15:00	Break
15:30	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