Call for Participation:  NFM 2018
Tenth NASA Formal Methods Symposium
30 Years of Formal Methods at NASA
April 17-19, Newport News, VA, USA
Celebrating 30 years of formal methods research at NASA Langley, the
Tenth NASA Formal Methods Symposium (NFM) is a forum to foster
collaboration between theoreticians and practitioners from NASA,
academia, and industry. NFM's goals are to identify challenges and to
provide solutions for achieving assurance for such critical systems.
Keynote speakers:
  Ricky Butler (NASA, USA)
  Gilles Dowek (INRIA, CNRS, École Normale Supérieure Paris-Saclay, France)
The program of symposium is available at:
Attendance to the symposium is free, but all attendees must register in order 
to participate.
Registrations are open until ** April 1, 2018 ** at:

The symposium will be held at
  Newport News Marriott at City Center
  740 Town Center Drive
  Newport News, VA 23606, USA.
  Phone: +1 (757) 873-9299. 

A group rate to attend NFM2018 is available at the Newport News
Marriot until ** March 16, 2018 **. Reservations can be made by calling
+1 (866) 329-1758, and asking for the group code: NASA, or through
web at

List of Accepted Papers:
* Ansgar Fehnker, Kaylash Chaudhary and Vinay Mehta. An Even Better Approach - 
   the B.A.T.M.A.N. Protocol Through Formal Modelling and Analysis 
* Massimo Narizzano, Luca Pulina, Armando Tacchella and Simone Vuotto. 
Consistency of
  Property Specification Patterns with Boolean and Constrained Numerical Signals
* Marcus Gerhold, Arnd Hartmanns and Mariëlle Stoelinga. Model-Based Testing 
for General
  Stochastic Time
* Ruben Giaquinta, Ruth Hoffmann, Murray Ireland, Alice Miller, and Gethin 
Norman. Strategy
  Synthesis for Autonomous Agents using PRISM
* Miguel Romero and Camilo Rocha. Symbolic Execution and Reachability Analysis 
  Rewriting Modulo SMT for Spatial Concurrent Constraint Systems with Extrusion
* Lola Masson, Jérémie Guiochet, Helene Waeselynck, Martin Törngren, Sofia 
Cassel and Kalou
  Cabrera. Tuning permissiveness of active safety monitors for autonomous 
* Radha Nakade, Eric Mercer, Peter Aldous and Jay McCarthy. Model Checking Task 
  Programs for Data-race
* Aymeric Fromherz, Abdelraouf Ouadjaout and Antoine Miné. Static Value 
Analysis of Python
  Programs by Abstract Interpretation
* Flavio M. de Paula, Arvind Haran and Brad Bingham. An Efficient Rewriting 
Framework for
  Trace Coverage of Symmetric Systems
* Ansgar Fehnker and Kaylash Chaudhary. Twenty Percent and a Few Days - 
Optimising a
  Bitcoin Majority Attack (short paper)
* Jeroen Meijer and Jaco van de Pol. Sound Black-Box Checking in the LearnLib
* Philipp Koerner and Jens Bendisposto. Distributed Model Checking Using ProB
* Saksham Chand and Yanhong A. Liu. Simpler Specifications and Easier Proofs of 
  Algorithms Using History Variables
* Siddhartha Bhattacharyya, Thomas Eskridge, Natasha Neogi, Marco Carvalho and 
  Stafford. Formal Assurance for Cooperative Intelligent Autonomous Agents
* Yassmeen Elderhalli, Osman Hasan, Waqar Ahmed and Sofiène Tahar. Formal 
Dynamic Fault
  Trees Analysis using an Integration of Theorem Proving and Model Checking
* Sarah Benyagoub, Meriem Ouederni, Yamine Ait Ameur, and Atif Mashkoor. 
Incremental Construction of
  Realizable Choreographies
* César Augusto Ochoa Escudero, Rémi Delmas, Thomas Bochot, Matthieu
   David, and Virginie Wiels. Automatic Generation of DO-178 Test Procedures
* Andrew Ireland, Maria Teresa Llano and Simon Colton. The Use of Automated 
  Formation in Support of Hazard Analysis (short paper)
* Zhuo Chen and Werner Dietl. Don't Miss the End: Preventing Unsafe End-of-File 
Comparisons (short paper)
* András Vörös, Márton Búr, István Ráth, Ákos Horváth, Zoltán Micskei, László 
Balogh, Bálint Hegyi, Benedek Horváth, 
  Zsolt Mázló and Dániel Varró. MoDeS3: Model-based Demonstrator for Smart and 
Safe Cyber-Physical Systems (short paper)
* Giovanna Broccia, Paolo Milazzo and Peter Csaba Ölveczky. An Executable 
Formal Framework
  for Safety-Critical Human Multitasking
* Marco Feliú and Mariano Moscato. Towards a Formal Safety Framework for 
Trajectories (short paper)
* Rui Qiu, Sarfraz Khurshid, Corina Pasareanu, Junye Wen and Guowei Yang. Using 
Test Ranges
  to Improve Symbolic Execution
* Allan Blanchard, Nikolai Kosmatov and Frédéric Loulergue. Ghosts for Lists: A 
Critical Module
  of Contiki Verified in Frama-C
* Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan and Ashish Tiwari. 
Output Range Analysis for
  Deep Feedforward Neural Networks
* Bruno Dutertre, Dejan Jovanović and Jorge Navas. Verification of 
Fault-Tolerant Protocols
  with Sally (short paper)
* Alfons Laarman. Optimal Storage of Combinatorial State Spaces
* Alfons Laarman. Stubborn Transaction Reduction
* Cumhur Erkan Tuncali, Bardh Hoxha, Guohui Ding, Georgios Fainekos and Sriram
  Sankaranarayanan. Experience Report: Application of Falsification Methods on 
the UxAS
  System (short paper)
* Hendrik Maarand and Tarmo Uustalu. Certified Foata Normalization for 
Generalized Traces
* Francesco Marconi, Giovanni Quattrocchi, Luciano Baresi, Marcello M. Bersani 
and Matteo
  Rossi. On the Timed Analysis of Big-Data Applications

Organizing Committee
Anthony Narkawicz (Conference Chair)
Aaron Dutle (Program Co-Chair)
Cesar Munoz (Program Co-Chair)

Email: nfm2018 [at] easychair [dot] org
Web: https://shemesh.larc.nasa.gov/NFM2018/

To opt-out from this mailing list, send an email to


with the word 'unsubscribe' as subject or in the body. You can also make the 
request by contacting

Om-announce mailing list

Reply via email to