NASA Logo, National Aeronautics and Space Administration
Intelligent Systems Division Banner

NFM-2017 Accepted Papers

Kim Völlinger and Samira Akili. Verifying a Class of Certifying Distributed Programs
Brandon Shapiro and Chris Casinghino. specgen: A Tool for Modeling Statecharts in CSP
Aaron Fifarek, Lucas Wagner, Erika Hoffman, Benjamin Rodes, M. Anthony Aiello and Jennifer Davis. SpeAR v2.0: Formalized Past LTL Specification and Analysis of Requirements
Hugo Daniel Macedo, Anne E. Haxthausen and Alessandro Fantechi. Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations
Hugo Illous, Matthieu Lemerre and Xavier Rival. A Relational Shape Abstract Domain
Mario Gleirscher and Stefan Kugele. From Hazard Analysis to Hazard Mitigation Planning: The Automated Driving Case
Saeed Darabi, Stefan Blom and Marieke Huisman. A Verification Technique for Deterministic Parallel Programs
Hadar Frenkel, Orna Grumberg and Sarai Sheinvald. An Automata-Theoretic Approach to Modeling Systems and Specifications Over Infinite Data
Arnaud Dieumegard, Ning Ge and Eric Jenn. Event-B at Work: some Lessons Learnt from an Application to a Robot Anti-Collision Function
Stefan Schupp, Erika Abraham, Ibtissem Ben Makhlouf and Stefan Kowalewski. HyPro: A C++ library for state set representations for hybrid systems reachability analysis
Silvia Bonfanti, Marco Carissoni, Angelo Gargantini and Atif Mashkoor. Asm2C++: a tool for Code Generation from Abstract State Machines to Arduino
Marie-Christine Jakobs and Heike Wehrheim. Compact Proof Witnesses
Braham Lotfi Mediouni, Ayoub Nouri, Marius Bozga and Saddek Bensalem. Improved Learning for Stochastic Timed Models by State-Merging Algorithms
Andrew Sogokon, Paul Jackson and Taylor T Johnson. Verifying safety and persistence properties of hybrid systems using flowpipes and continuous invariants
Seth Ahrenbach. Reasoning About Safety-Critical Information Flow Between Pilot and Computer
Bernhard K. Aichernig and Martin Tappler. Learning from Faults: Mutation Testing in Active Automata Learning
Claire Dross and Yannick Moy. Auto-Active Proof of Red-Black Trees in SPARK
Levi Lucio, Chih-Hong Cheng, Salman Rahman and Alistair Mavin. Just Formal Enough? Automated Analysis of EARS Requirements
Colin Snook, Thai Son Hoang and Michael Butler. Analysing Security Protocols Using Refinement in iUML-B
Yulia Demyanova, Philipp Ruemmer and Florian Zuleger. Systematic Predicate Abstraction using Variable Roles
Mateus Borges, Quoc-Sang Phan, Antonio Filieri and Corina Pasareanu. Model-counting approaches for nonlinear numerical constraints
Lucas Wagner, Alain Mebsout, Cesare Tinelli, Darren Cofer and Konrad Slind. Qualification of a Model Checker for Avionics Software Verification
Hoang Gia Nguyen, Étienne André, Laure Petrucci and Jun Sun. Parametric model checking timed automata under non-Zenoness assumption
Constantin Enea, Ondrej Lengal, Mihaela Sighireanu and Tomas Vojnar. SPEN: A Solver for Separation Logic
Lee Pike and Benjamin Jones. Modular Model-Checking of a Byzantine Fault-Tolerant Protocol
Susmit Jha, Vasumathi Raman, Alessandro Pinto, Tuhin Sahai and Michael Francis. On Learning Sparse Boolean Formulae For Explaining AI Decisions
Ashlie B. Hocking, M. Anthony Aiello, John C. Knight and Nikos Aréchiga. Input Space Partitioning to Enable Massively Parallel Proof
Tommaso Dreossi, Alexandre Donzé and Sanjit Seshia. Compositional Falsification of Cyber-Physical Systems with Machine Learning Components
James Ortiz, Moussa Amrani and Pierre-Yves Schobbens. Multi-Timed Bisimulation for Distributed Timed Automata
Matteo Camilli, Carlo Bellettini, Angelo Gargantini and Patrizia Scandurra. Event-based Runtime Verification of Temporal Properties using Time Basic Petri Nets
Matthieu Martel. Floating-Point Format Inference in Mixed-Precision

General Chair

Misty Davies
(NASA Ames)

Program Chairs

Clark Barrett
(Stanford University)

Temesghen Kahsai
(NASA Ames / CMU)

Local organization

Guy Katz
(Stanford University)

Rody Kersten
(CMU Silicon Valley)

Program Committee

Aarti Gupta (Princeton)
Alberto Griggio (FBK-IRST)
Alessandro Cimatti (FBK-IRST)
Alwyn Goodloe (NASA Langley)
Arie Gurfinkel (University of Waterloo)
Cesare Tinelli (University of Iowa)
Christoph Torens (German Aerospace Center)
Daniel Kroening (University of Oxford)
Dejan Jovanović (SRI)
Dino Distefano (Facebook)
Dirk Beyer (LMU Munich)
Domagoj Babic (Google)
Ella Atkins (University of Michigan)
Eric Feron (Georgia Tech)
Ewen Denney (SGT / NASA Ames)
Gerwin Klein (NICTA and UNSW)
John Harrison (Intel)
John Rushby (SRI)
Jorge Navas (SRI)
Julia Badger (NASA)
Kalou Cabrera Castillos (LAAS-CNRS)
Kelly Hayhurst (NASA)
Kirstie L. Bellman (The Aerospace Corporation)
Klaus Havelund (NASA JPL)
Kristin Yvonne Rozier (Iowa State University)
Lael Rudd (Draper)
Lee Pike (Galois)
Martin Schäf (SRI)
Mats Heimdahl (University of Minnesota)
Meeko Oishi (University of New Mexico)
Mike Hinchey (Lero-the Irish Software Engineering Research Centre)
Michael Lowry (NASA Ames)
Murali Rangarajan (Boeing)
Natasha Neogi (NASA Langley)
Neha Rungta (AWS)
Nikolaj Bjorner (Microsoft Research)
Patrice Godefroid (Microsoft Research)
Philipp Ruemmer (Uppsala University)
Pierre-Loïc Garoche (ONERA)
Rajeev Joshi (NASA JPL)
Sriram Sankaranarayanan (University of Colorado Boulder)
Susmit Jha (United Technologies)
Virginie Wiels (ONERA)
Wenchao Li (Boston University)
Zvonimir Rakamaric (University of Utah)

First Gov logo
NASA Logo - nasa.gov