


default search action
14th NFM 2022: Pasadena, CA, USA
- Jyotirmoy V. Deshmukh
, Klaus Havelund
, Ivan Perez
:
NASA Formal Methods - 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24-27, 2022, Proceedings. Lecture Notes in Computer Science 13260, Springer 2022, ISBN 978-3-031-06772-3
Invited Keynotes
- Steve A. Chien
:
Formal Methods for Trusted Space Autonomy: Boon or Bane? 3-13 - Dines Bjørner:
An Essence of Domain Engineering - A Basis for Trustworthy Aeronautics and Space Software. 14-51 - Daniel Jackson:
Concept Design Moves. 52-70 - Julia Lawall
, Gilles Muller
:
Automating Program Transformation with Coccinelle. 71-87 - Vytautas Astrauskas, Aurel Bílý, Jonás Fiala, Zachary Grannan, Christoph Matheja, Peter Müller, Federico Poli
, Alexander J. Summers:
The Prusti Project: Formal Verification for Rust. 88-108 - Xin Chen, Sriram Sankaranarayanan:
Reachability Analysis for Cyber-Physical Systems: Are We There Yet? 109-130
Regular Submissions
- Josefine Graebener, Apurva Badithela, Richard M. Murray:
Towards Better Test Coverage: Merging Unit Tests for Autonomous Systemsđagger . 133-155 - Holger Hermanns, Gilles Nies:
Quantification of Battery Depletion Risk Made Efficient. 156-174 - Timothy E. Wang, Zamira Daw, Pierluigi Nuzzo, Alessandro Pinto
:
Hierarchical Contract-Based Synthesis for Assurance Cases. 175-192 - Edoardo Bacci
, David Parker
:
Verified Probabilistic Policies for Deep Reinforcement Learning. 193-212 - Ulices Santa Cruz, Yasser Shoukry
:
NNLander-VeriF: A Neural Network Formal Verification Framework for Vision-Based Autonomous Aircraft Landing. 213-230 - Usama Mehmood, Sanaz Sheikhi, Stanley Bak, Scott A. Smolka, Scott D. Stoller:
The Black-Box Simplex Architecture for Runtime Assurance of Autonomous CPS. 231-250 - Yue Meng, Zeng Qiu, Md Tawhid Bin Waez, Chuchu Fan:
Case Studies for Computing Density of Reachable States for Safe Autonomous Motion Planning. 251-271 - Marie Farrell, Matt Luckcuck
, Oisín Sheridan, Rosemary Monahan:
Towards Refactoring FRETish Requirements. 272-279 - Stanley Bak, Hoang-Dung Tran:
Neural Network Compression of ACAS Xu Early Prototype Is Unsafe: Closed-Loop Verification Through Quantized State Backreachability. 280-298 - Christopher A. Strong, Sydney M. Katz, Anthony L. Corso
, Mykel J. Kochenderfer
:
ZoPE: A Fast Optimizer for ReLU Networks with Low-Dimensional Inputs. 299-317 - Diganta Mukhopadhyay, Kumar Madhukar, Mandayam K. Srivas:
Permutation Invariance of Deep Neural Networks with ReLUs. 318-337 - Xaver Fink
, Philipp Berger
, Joost-Pieter Katoen
:
Configurable Benchmarks for C Model Checkers. 338-354 - Cong Liu, Junaid Babar, Isaac Amundson, Karl Hoech, Darren D. Cofer, Eric Mercer
:
Assume-Guarantee Reasoning with Scheduled Components. 355-372 - Andrea Pferscher, Bernhard K. Aichernig
:
Stateful Black-Box Fuzzing of Bluetooth Devices Using Automata Learning. 373-392 - Jad Hamza, Simon Felix
, Viktor Kuncak
, Ivo Nussbaumer, Filip Schramka:
From Verified Scala to STIX File System Embedded Code Using Stainless. 393-410 - Étienne Payet
, David J. Pearce
, Fausto Spoto
:
On the Termination of Borrow Checking in Featherweight Rust. 411-430 - James Noble
, David Streader, Isaac Oscar Gariano
, Miniruwani Samarakoon:
More Programming Than Programming: Teaching Formal Methods in a Software Engineering Programme. 431-450 - Johan Arcile, Étienne André
:
Zone Extrapolations in Parametric Timed Automata. 451-469 - Étienne André
, Masaki Waga
, Natsuki Urabe
, Ichiro Hasuo
:
Exemplifying Parametric Timed Specifications over Signals with Bounded Behavior. 470-488 - Martin Tappler, Bernhard K. Aichernig, Florian Lorber:
Timed Automata Learning via SMT Solving. 489-507 - Alberto Bombardelli
, Stefano Tonetta
:
Asynchronous Composition of Local Interface LTL Properties. 508-526 - Zachary Luppen
, Michael Jacks
, Nathan Baughman
, Muhamed Stilic
, Ryan Nasers
, Benjamin Hertz
, James W. Cutler
, Dae Young Lee
, Kristin Yvonne Rozier
:
Elucidation and Analysis of Specification Patterns in Aerospace System Telemetry. 527-537 - Satya Prakash Nayak
, Daniel Neider
, Rajarshi Roy
, Martin Zimmermann
:
Robust Computation Tree Logic. 538-556 - Ruiyang Xu
, Karl J. Lieberherr
:
On-the-Fly Model Checking with Neural MCTS. 557-575 - Devesh Bhatt, Hao Ren, Anitha Murugesan, Jason Biatek, Srivatsan Varadarajan, Natarajan Shankar:
Requirements-Driven Model Checking and Test Generation for Comprehensive Verification. 576-596 - Paul C. Attie
:
Operational Annotations - A New Method for Sequential Program Verification. 597-615 - Harold Carr, Christa Jenkins, Mark Moir, Victor Cacciari Miraldo, Lisandra Silva:
Towards Formal Verification of HotStuff-Based Byzantine Fault Tolerant Consensus in Agda. 616-635 - Xiaoxin An, Freek Verbeek, Binoy Ravindran:
DSV: Disassembly Soundness Validation Without Assuming a Ground Truth. 636-655 - Oyendrila Dobe, Lukas Wilke, Erika Ábrahám
, Ezio Bartocci
, Borzoo Bonakdarpour:
Probabilistic Hyperproperties with Rewards. 656-673 - Inigo Incer
, Albert Benveniste, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia:
Hypercontracts. 674-692 - Felipe Gorostiaga, César Sánchez
:
Monitorability of Expressive Verdicts. 693-712 - Daniel Basgöze, Matthias Volk
, Joost-Pieter Katoen
, Shahid Khan
, Mariëlle Stoelinga
:
BDDs Strike Back - Efficient Analysis of Static and Dynamic Fault Trees. 713-732 - Daisuke Ishii, Takashi Tomita
, Toshiaki Aoki
:
Approximate Translation from Floating-Point to Real-Interval Arithmetic. 733-751 - Baoluo Meng
, Arjun Viswanathan, William Smith, Abha Moitra, Kit Siu, Michael Durling:
Synthesis of Optimal Defenses for System Architecture Design Model in MaxSMT. 752-770 - Michal Konecný
, Sewon Park
, Holger Thies
:
Certified Computation of Nondeterministic Limits. 771-789 - Lieuwe Vinkhuijzen
, Alfons Laarman
:
The Power of Disjoint Support Decompositions in Decision Diagrams. 790-799 - Kenny Ballou
, Elena Sherman
:
Incremental Transitive Closure for Zonal Abstract Domain. 800-808 - Paolo Masci, Aaron Dutle:
Proof Mate: An Interactive Proof Helper for PVS (Tool Paper). 809-815 - Alexis A. Aurandt
, Phillip H. Jones
, Kristin Yvonne Rozier
:
Runtime Verification Triggers Real-Time, Autonomous Fault Recovery on the CySat-I. 816-825

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.