Friday, November 18

9:30-11:00 Keynote I: How to Prove Hybrid Systems
Andr´ Platzer, Carnegie Mellon University
11:00-11:30Coffee Break
11:30-12:00 Formal Feature Analysis of Hybrid Automata
Antonio Bruto Da Costa, Pallab Dasgupta, and Goran Frehse
12:00-12:30 Parallel Reachability Analysis for Hybrid Systems
Amit Gurung, Arup Kumar Deka, Ezio Bartocci, Sergiy Bogomolov, Radu Grosu, and Rajarshi Ray
12:30-13:00 Control-flow Guided Property Directed Reachability for Imperative Synchronous Programs
Xian Li and Klaus Schneider
13:00-14:00Lunch Break
14:00-14:30 A Computer-Algebraic Approach to Formal Verification of Data-Centric Low-Level Software
Oliver Marx, Carlos Villarraga, Dominik Stoffel, and Wolfgang Kunz
14:30-15:00 Verifying the Concentration Property of Permutation Networks by BDDs
Tripti Jain and Klaus Schneider
15:00-15:30Coffee Break
15:30-15:45 Combining Type Checking with Model Checking for System Verification
Zhiqiang Ren and Hongwei Xi
15:45-16:00 Formal Engineering Frameworks in Maritime Domain Awareness
Amir Yaghoubi Shahir, Uwe Glässer, Hamed Yaghoubi Shahir, Mohammad Ali Tayebi, and Hans Wehn
16:00-16:15 Frame Conditions in Symbolic Representations of UML/OCL Models
Nils Przigoda, Jonas Gomes Filho, Philipp Niemann, Robert Wille, and Rolf Drechsler
16:15-16:30 Towards Integrating Statistical Model Checking into Property-Based Testing
Bernhard K. Aichernig and Richard Schumi
16:30-18:00 Discussion at Posters

Saturday, November 19

9:30-11:00 Keynote II: Multiform Logical Time for Me/Mo-codesign
Robert de Simone, INRIA
11:00-11:30Coffee Break
11:30-12:00 Clocks vs. Instants Relations: Verifying CCSL Time Constraints in UML/MARTE Models
Judith Peters, Nils Przigoda, Robert Wille, and Rolf Drechsler
12:00-12:30 Specification of Precise Timing in Synchronous Dataflow Models
Patricia Derler, Kaushik Ravindran, and Rhishikesh Limaye
12:30-13:00 Specification, Verification, and Synthesis using Extended State Machines with Callbacks
Farhaan Fowze and Tuba Yavuz
13:00-14:00Lunch Break
14:00-14:30 Performance-aware Scheduling of Multicore Time-critical Systems
Jalil Boudjadar, Jin Hyun Kim, and Simin Nadjm-Tehrani
14:30-15:00 Accelerating Schedule Space Exploration of Multi-threaded Programs with GPUs
Prakhar Banga, Atul Pai, Subhajit Roy, and Mainak Chaudhuri
15:00-15:30Coffee Break
15:30-15:45 MEMOCODE 2016 Design Contest: k-Means Clustering
Peter Milder
15:45-16:15 An Efficient Multi-core and Many-core Implementation of K-Means Clustering
Saeid Rahmani, Armin Ahmadzadeh, Omid Hajihassani, SeyedPooya Mirhosseini, and Saeid Gorgin
16:15-16:30 SmashClean: A Hardware level mitigation to stack smashing attacks in OpenRISC
Manaar Alam, Debapriya Basu Roy, Sarani Bhattacharya, Vidya Govindan, Rajat Subhra Chakraborty, and Debdeep Mukhopadhyay
16:30-16:45 GANDALF: A fine-grained hardware-software co-design for preventing memory attacks
Prasanna Karthik, Patanjali SLPSK, Gnanambikai Krishnakumar, and Chester Rebeiro
20:00-22:30Conference Banquet

Sunday, November 20

9:30-11:00 Keynote III: Trusted Cloud: How to make the cloud more secure
Sriram Rajamani, Microsoft Research
11:00-11:30Coffee Break
11:30-12:00 Verification of Component Architectures using Mode-Based Contracts
Stefan Kugele, Diego Marmsoler, N&ucute;ria Mata, and Kai Werther
12:00-12:30 Optimal Compilation for Exposed Datapath Architectures with Buffered Processing Units by SAT Solvers
Anoop Bhagyanath and Klaus Schneider
12:30-13:00 A formal approach to the mapping of tasks on an heterogenous multicore, energy-aware architecture
Emilien Kofman and Robert de Simone
13:00-14:00Lunch Break
14:00-14:30 Asynchrony-Aware Static Analysis of Android Applications
Ashish Mishra, Aditya Kanade, and Y.N. Srikant
14:30-15:00 Step Revision in Hybrid Co-simulation with FMI
Fabio Cremona, Marten Lohstroh, David Broman, Marco Di Natale, Edward Lee, and Stavros Tripakis
15:00-15:30 An Efficient Algorithm for Monitoring Practical TPTL Specifications
Adel Dokhanchi, Bardh Hoxha, Cumhur Erkan Tuncali, and Georgios Fainekos
15:30-15:45Closing Remarks