17-19 Apr 2018
Newport News VA, U.S.A.
-----------------------------------------
Call for Participation: NFM 2018
-----------------------------------------
Tenth NASA Formal Methods Symposium
30 Years of Formal Methods at NASA
April 17-19, Newport News, VA, USA
https://shemesh.larc.nasa.gov/NFM2018/
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:
https://shemesh.larc.nasa.gov/NFM2018/program.html
Attendance to the symposium is free, but all attendees must register in order to participate.
Registrations are open until ** April 1, 2018 ** at:
https://shemesh.larc.nasa.gov/NFM2018/registration.html
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
https://shemesh.larc.nasa.gov/NFM2018/hotel_reservation.html
List of Accepted Papers:
* Ansgar Fehnker, Kaylash Chaudhary and Vinay Mehta. An Even Better Approach - Improving
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 using
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 systems
* Radha Nakade, Eric Mercer, Peter Aldous and Jay McCarthy. Model Checking Task Parallel
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 Distributed
Algorithms Using History Variables
* Siddhartha Bhattacharyya, Thomas Eskridge, Natasha Neogi, Marco Carvalho and Milton
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 Theory
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)
Contact
--------
Email: nfm2018 [at] easychair [dot] org
Web: https://shemesh.larc.nasa.gov/NFM2018/
--
[LOGIC] mailing list
http://www.dvmlg.de/mailingliste.html
Archive: http://www.illc.uva.nl/LogicList/
provided by a collaboration of the DVMLG, the Maths Departments in Bonn and Hamburg, and the ILLC at the Universiteit van Amsterdam