NASA
JPL
Caltech
NASA JPL Logo
NASA Logo

NASA Formal Methods 2022 - Accepted papers

Density of Reachable States and How to Use it for Safe Autonomous Motion Planning Yue Meng, Zeng Qiu, Md Tawhid Bin Waez and Chuchu Fan.
From Verified Scala to STIX File System Embedded Code using Stainless Jad Hamza, Simon Felix, Viktor Kuncak, Ivo Nussbaumer and Filip Schramka.
Operational annotations: a new method for sequential program verification Paul Attie.
Robust Computation Tree Logic Satya Prakash Nayak, Daniel Neider, Rajarshi Roy and Martin Zimmermann.
Zone extrapolations in parametric timed automata Johan Arcile and Étienne André.
More Programming Than Programming: Teaching Formal Methods in a Software Engineering Programme James Noble, David Streader, Isaac Oscar Gariano and Miniruwani Samarakoon.
Towards Refactoring FRETish Requirements Marie Farrell, Matt Luckcuck, Oisin Sheridan and Rosemary Monahan.
Towards Formal Verification of HotStuff-based Byzantine Fault Tolerant Consensus in Agda Harold Carr, Christopher Jenkins, Mark Moir, Victor Cacciari Miraldo and Lisandra Silva.
Assume-Guarantee Reasoning with Scheduled Components Cong Liu, Junaid Babar, Isaac Amundson, Karl Hoech, Darren Cofer and Eric Mercer.
On-the-Fly Model Checking with Neural MCTS Ruiyang Xu and Karl Lieberherr.
Permutation Invariance of Deep Neural Networks with ReLUs Diganta Mukhopadhyay, Kumar Madhukar and Mandayam Srivas.
On the Termination of Borrow Checking in Featherweight Rust Etienne Payet, David J. Pearce and Fausto Spoto.
The Black-Box Simplex Architecture for Runtime Assurance of Autonomous CPS Usama Mehmood, Sanaz Sheikhi, Stanley Bak, Scott Smolka and Scott Stoller.
Towards Better Test Coverage: Merging Unit Tests for Autonomous Systems Josefine Graebener, Apurva Badithela and Richard Murray.
DSV: Disassembly Soundness Validation without Assuming a Ground Truth Xiaoxin An, Freek Verbeek and Binoy Ravindran.
Closed-Loop ACAS Xu NNCS is Unsafe: Quantized State Backreachability for Verification Stanley Bak and Hoang Dung Tran.
Approximate Translation from Floating-Point to Real-Interval Arithmetic Daisuke Ishii, Takashi Tomita and Toshiaki Aoki.
Hierarchical Contract-based Synthesis for Assurance Cases Timothy Wang, Zamira Daw, Pierluigi Nuzzo and Alessandro Pinto.
Stateful Black-Box Fuzzing of Bluetooth Devices Using Automata Learning Andrea Pferscher and Bernhard K. Aichernig.
Quantification of Battery Depletion Risk Made Efficient Gilles Nies and Holger Hermanns.
Configurable Benchmarks for C Model Checkers Xaver Fink, Philipp Berger and Joost-Pieter Katoen.
Timed Automata Learning via SMT Solving Martin Tappler, Bernhard K. Aichernig and Florian Lorber.
Verified Probabilistic Policies for Deep Reinforcement Learning Edoardo Bacci and David Parker.
Asynchronous Composition of Local Interface LTL Properties Alberto Bombardelli and Stefano Tonetta.
Daniel Basgöze, Matthias Volk, Joost-Pieter Katoen, Shahid Khan and Marielle Stoelinga. BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees
Exemplifying parametric timed specifications over signals with bounded behavior Étienne André, Masaki Waga, Natsuki Urabe and Ichiro Hasuo.
Monitorability of Expressive Verdicts Felipe Gorostiaga and Cesar Sanchez.
Requirements-Driven Model Checking and Test Generation for Comprehensive Verification Devesh Bhatt, Hao Ren, Anitha Murugesan, Jason Biatek, Srivatsan Varadarajan and Natrajan Shankar.
Probabilistic Hyperproperties with Rewards Lukas Wilke, Oyendrila Dobe, Erika Ábrahám, Ezio Bartocci and Borzoo Bonakdarpour.
Hypercontracts Inigo Incer, Albert Benveniste, Alberto Sangiovanni-Vincentelli and Sanjit Seshia.
Elucidation and Analysis of Specification Patterns in Aerospace System Telemetry Zachary Luppen, Michael Jacks, Nathan Baughman, Muhamed Stilic, Ryan Nasers, Benjamin Hertz, James Cutler, Dae Young Lee and Kristin Yvonne Rozier.
Runtime Verification Triggers Real-time, Autonomous Fault Recovery on the CySat-I Alexis Aurandt, Phillip Jones and Kristin Yvonne Rozier.
Incremental Transitive Closure for Zonal Abstract Domain Kenny Ballou and Elena Sherman.
NNLander-VeriF: A Neural Network Formal Verification Framework for Vision-Based Autonomous Aircraft Landing Ulices Santa Cruz Leal and Yasser Shoukry.
The Power of Disjoint Support Decompositions in Decision Diagrams Lieuwe Vinkhuijzen and Alfons Laarman.
Proof Mate: an Interactive Proof Helper for PVS Paolo Masci and Aaron Dutle.
Certified Computation of Nondeterministic Limits Michal Konecny, Sewon Park and Holger Thies.
ZoPE: A Fast Optimizer for ReLU Networks with Low-Dimensional Inputs Christopher Strong, Sydney Katz, Anthony Corso and Mykel Kochenderfer.
Synthesis of Optimal Defenses for System Architecture Design Model in MaxSMT Baoluo Meng, Arjun Viswanathan, William Smith, Abha Moitra, Kit Siu and Michael Durling.

NASA
JPL
Caltech
Site Editors: Klaus Havelund (JPL), Ivan Perez (NIA)