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

May 16, 2017

7:00-8:00 Registration
8:00-8:30 Welcome
8:30-9:30 Invited Talk: Jason Crusan, NASA
9:30-10:00 Break
10:00-12:00 Paper Session: Automata
Hadar Frenkel, Orna Grumberg and Sarai Sheinvald. An Automata-Theoretic Approach to Modeling Systems and Specifications Over Infinite Data.
Bernhard K. Aichernig and Martin Tappler. Learning from Faults: Mutation Testing in Active Automata Learning.
Hoang Gia Nguyen, Étienne André, Laure Petrucci and Jun Sun. Parametric model checking timed automata under non-Zenoness assumption.
James Ortiz, Moussa Amrani and Pierre-Yves Schobbens. Multi-Timed Bisimulation for Distributed Timed Automata
12:00-1:30 Lunch
1:30-2:30 Invited Talk: Michael Wagner, CMU
2:30-3:00 Break
3:00-5:30 Paper Session: Logic and Verification
Claire Dross and Yannick Moy. Auto-Active Proof of Red-Black Trees in SPARK.
Colin Snook, Thai Son Hoang and Michael Butler. Analysing Security Protocols Using Refinement in iUML-B.
Susmit Jha, Vasumathi Raman, Alessandro Pinto, Tuhin Sahai and Michael Francis. On Learning Sparse Boolean Formulae For Explaining AI Decisions.
Matteo Camilli, Carlo Bellettini, Angelo Gargantini and Patrizia Scandurra. Event-based Runtime Verification of Temporal Properties using Time Basic Petri Nets.
Mateus Borges, Quoc-Sang Phan, Antonio Filieri and Corina Pasareanu. Model-counting approaches for nonlinear numerical constraints. (short)
Ashlie B. Hocking, M. Anthony Aiello, John C. Knight and Nikos Aréchiga. Input Space Partitioning to Enable Massively Parallel Proof. (short)

May 17, 2017

8:30-9:30 Invited Talk: Ben Haldeman, Planet
9:30-10:00 Break
10:00-11:00 Paper Session: Model Checking
Hugo Daniel Macedo, Anne E. Haxthausen and Alessandro Fantechi. Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations.
Lee Pike and Benjamin Jones. Modular Model-Checking of a Byzantine Fault-Tolerant Protocol.
11:00-12:00 Paper Session: Quantitative Analysis
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.
12:00-1:30 Lunch
1:30-2:30 Paper Session: Abstract Interpretation
Hugo Illous, Matthieu Lemerre and Xavier Rival. A Relational Shape Abstract Domain.
Matthieu Martel. Floating-Point Format Inference in Mixed-Precision.
2:30-3:30 Paper Session: Static Analysis
Saeed Darabi, Stefan Blom and Marieke Huisman. A Verification Technique for Deterministic Parallel Programs.
Yulia Demyanova, Philipp Ruemmer and Florian Zuleger. Systematic Predicate Abstraction using Variable Roles.
3:30-4:00 Break
4:00-5:00 Paper Session: Tool Papers
Brandon Shapiro and Chris Casinghino. specgen: A Tool for Modeling Statecharts in CSP. (short)
Stefan Schupp, Erika Abraham, Ibtissem Ben Makhlouf and Stefan Kowalewski. HyPro: A C++ library for state set representations for hybrid systems reachability analysis. (short)
Silvia Bonfanti, Marco Carissoni, Angelo Gargantini and Atif Mashkoor. Asm2C++: a tool for Code Generation from Abstract State Machines to Arduino. (short)
Constantin Enea, Ondrej Lengal, Mihaela Sighireanu and Tomas Vojnar. SPEN: A Solver for Separation Logic. (short)
5:00-6:00 Panel and Discussion: Fostering Collaboration Through Real-World Benchmarks.

May 18, 2017

8:30-9:30 Invited Talk: Manu Sridharan, Uber
9:30-10:00 Break
10:00-12:00 Paper Session: Applications of Formal Methods
Mario Gleirscher and Stefan Kugele. From Hazard Analysis to Hazard Mitigation Planning: The Automated Driving Case.
Arnaud Dieumegard, Ning Ge and Eric Jenn. Event-B at Work: some Lessons Learnt from an Application to a Robot Anti-Collision Function.
Seth Ahrenbach. Reasoning About Safety-Critical Information Flow Between Pilot and Computer.
Tommaso Dreossi, Alexandre Donzé and Sanjit Seshia. Compositional Falsification of Cyber-Physical Systems with Machine Learning Components.
12:00-1:30 Lunch
1:30-2:30 Invited Talk: Alexandre Arnold, Airbus
2:30-3:00 Break
3:00-4:30 Paper Session: Proofs and Certificates
Kim Völlinger and Samira Akili. Verifying a Class of Certifying Distributed Programs.
Marie-Christine Jakobs and Heike Wehrheim. Compact Proof Witnesses.
Lucas Wagner, Alain Mebsout, Cesare Tinelli, Darren Cofer and Konrad Slind. Qualification of a Model Checker for Avionics Software Verification.
4:30-5:00 Paper Session: Requirements
Aaron Fifarek, Lucas Wagner, Erika Hoffman, Benjamin Rodes, M. Anthony Aiello and Jennifer Davis. SpeAR v2.0: Formalized Past LTL Specication and Analysis of Requirements. (short)
Levi Lucio, Chih-Hong Cheng, Salman Rahman and Alistair Mavin. Just Formal Enough? Automated Analysis of EARS Requirements. (short)
5:00-5:30 Closing Remarks and NFM-2018
First Gov logo
NASA Logo -