Monday April 27 NASA Formal Methods Symposium 2015

08:15-08:45 Registration
08:45-09:00 Welcome
Invited talk — chaired by Rajeev Joshi
09:00-10:00 Rob Manning Complexity tolerance: dealing with faults of our own making
10:00-10:30 Coffee break
Session 1 — chaired by Saddek Bensalem
10:30-11:00 Martín Abadi and Michael Isard Timely Rollback: Specification and Verification
11:00-11:30 Aboubakr Achraf El Ghazi, Mana Taghdiri and Mihai Herda First-Order Transitive Closure Axiomatization via Iterative Invariant Injections
11:30-12:00 Gianluca Amato, Simone Di Nardo Di Maio and Francesca Scozzari Sum of Abstract Domains
12:00-01:30 Lunch
Session 2 — chaired by Borzoo Bonakdarpour
01:30-02:00 Étienne André, Giuseppe Lipari, Hoang Gia Nguyen and Youcheng Sun Reachability Preservation Based Parameter Synthesis for Timed Automata
02:00-02:30 Lacramioara Astefanoaei, Ben Rayana Souha, Saddek Bensalem, Marius Bozga and Jacques Combaz Compositional Verification of Parameterised Timed Systems
02:30-03:00 John Backes, Darren Cofer, Steven Miller and Michael Whalen Requirements Analysis of a Quad-Redundant Flight Control System
03:00-03:30 Coffee break
Session 3 — chaired by Oksana Tkachuk
03:30-04:00 Dragan Bosnacki and Mark Scheffer Partial Order Reduction and Symmetry with Multiple Representatives
04:00-04:30 Alice Dal Corso, Damiano Macedonio and Massimo Merro Statistical Model Checking of Ad Hoc Routing Protocols in Lossy Grid Networks
04:30-04:50 Ivan Bocic and Tevfik Bultan Data Model Bugs
04:50-05:10 Luis M. Carril and Walter F. Tichy Predicting and Witnessing Data Races using CSP
05:10-05:30 Xin Chen, Stefan Schupp, Ibtissem Ben Makhlouf, Erika Ábrahám, Goran Frehse and Stefan Kowalewski A Benchmark Suite for Hybrid Systems Reachability Analysis

Tuesday April 28 NASA Formal Methods Symposium 2015

Invited talk — chaired by Gerard Holzmann
09:00-10:00 Dino Distefano Moving fast with software verification
10:00-10:30 Coffee break
Session 4 — chaired by Kristin Rozier
10:30-11:00 Tommaso Dreossi, Thao Dang, Alexandre Donzé, James Kapinski, Jyotirmoy Deshmukh and Xiaoqing Jin Efficient Guiding Strategies for Testing of Temporal Properties of Hybrid Systems
11:00-11:30 Andrew Fisher, Chris Myers and Peng Li Reachability Analysis Using Extremal Rates
11:30-12:00 Andrew Gacek, Andreas Katis, Michael Whalen, John Backes and Darren Cofer Towards Realizability Checking of Contracts using Theories
12:00-01:30 Lunch
Session 5 — chaired by Neha Rungta
01:30-02:00 Thomas Gibson-Robinson, Henri Hansen, Bill Roscoe and Xu Wang Practical Partial Order Reduction for CSP
02:00-02:30 Alex Groce and Jervis Pinto A Little Language for Testing
02:30-03:00 Yu Huang and Eric Mercer Detecting MPI Zero Buffer Incompatibility by SMT Encoding
03:00-03:30 Coffee break
Session 6 — chaired by Alex Groce
03:30-04:00 Robert Jakob and Peter Thiemann A Falsification View of Success Typing
04:00-04:30 Wenrui Meng, Junkil Park, Oleg Sokolsky, Stephanie Weirich and Insup Lee Verified ROS-Based Deployment of Platform-Independent Control Systems
04:30-04:50 Jose Divasón and Jesus Aransay-Azofra Generalizing a Mathematical Analysis library in Isabelle/HOL
04:50-05:10 Graeme Gange, Jorge A Navas, Peter Schachte, Harald Sondergaard and Peter J Stuckey A Tool for Intersecting Context-Free Grammars and Its Applications
05:10-05:30 Reza Hajisheykhi, Ali Ebnenasir and Sandeep Kulkarni UFIT: A Tool for Modeling Faults in UPPAAL Timed Automata
07:30-10:00 Symposium dinner

Wednesday April 29 NASA Formal Methods Symposium 2015

Invited talk — chaired by Klaus Havelund
09:00-10:00 Viktor Kuncak Developing Verified Software Using Leon
10:00-10:30 Coffee break
Session 7 — chaired by Rahul Kumar
10:30-11:00 Rajiv Murali, Andrew Ireland and Gudmund Grov A Rigorous Approach to Combining Use Case Modelling and Accident Scenarios
11:00-11:30 Anitha Murugesan, Michael Whalen, Neha Rungta, Oksana Tkachuk, Suzette Person, Mats Heimdahl and Dongjiang You Are We There Yet? Determining the Adequacy of Formalized Requirements and Test Suites
11:30-12:00 Yan Peng and Mark Greenstreet Integrating SMT with Theorem Proving for Analog/Mixed-Signal Circuit Verification
12:00-01:30 Lunch
Session 8 — chaired by Richard DiFrancesco
01:30-02:00 Shashank Pathak, Erika Abraham, Nils Jansen, Armando Tacchella and Joost-Pieter Katoen A Greedy Approach for the Efficient Repair of Stochastic Models
02:00-02:30 Holger Siegel and Axel Simon Shape Analysis with Connectors
02:30-03:00 Daniel Schwartz-Narbonne, Martin Schäf, Dejan Jovanović, Philipp Rümmer and Thomas Wies Conflict-Directed Graph Coverage
03:00-03:30 Coffee break
Session 9 — chaired by Nikolaj Bjorner
03:30-04:00 Freek Verbeek, Julien Schmaltz, Sergey Tverdyshev, Holger Blasum, Oto Havle, Bruno Langenstein, Werner Stephan and Burkhart Wolff Formal Functional Specification of the PikeOS Separation Kernel
04:00-04:30 Ahlem Triki, Borzoo Bonakdarpour, Jacques Combaz and Saddek Bensalem Automated Conflict-Free Concurrent Implementation of Timed Component-Based Models
04:30-04:50 Marijn Heule, Martina Seidl and Armin Biere Blocked Literals are Universal
04:50-05:10 Howard Reubenstein, Greg Eakman, Tom Hawkins, Mitesh Jain and Panagiotis Manolios Practical Formal Verification of Domain-Specific Language Applications
05:10-05:30 Olli Saarikivi and Keijo Heljanko Reporting Races in Dynamic Partial Order Reduction