default search action
14th NFM 2022: Pasadena, CA, USA
- Jyotirmoy V. Deshmukh
, Klaus Havelund
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
Automating Program Transformation with Coccinelle. 71-87 - Vytautas Astrauskas, Aurel Bílý, Jonás Fiala, Zachary Grannan, Christoph Matheja, Peter Müller, Federico Poli
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
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
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
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
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
From Verified Scala to STIX File System Embedded Code Using Stainless. 393-410 - Étienne Payet
On the Termination of Borrow Checking in Featherweight Rust. 411-430 - James Noble
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é
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
Asynchronous Composition of Local Interface LTL Properties. 508-526 - Zachary Luppen
Elucidation and Analysis of Specification Patterns in Aerospace System Telemetry. 527-537 - Satya Prakash Nayak
Robust Computation Tree Logic. 538-556 - Ruiyang Xu
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
Probabilistic Hyperproperties with Rewards. 656-673 - Inigo Incer
Hypercontracts. 674-692 - Felipe Gorostiaga, César Sánchez
Monitorability of Expressive Verdicts. 693-712 - Daniel Basgöze, Matthias Volk
BDDs Strike Back - Efficient Analysis of Static and Dynamic Fault Trees. 713-732 - Daisuke Ishii, Takashi Tomita
Approximate Translation from Floating-Point to Real-Interval Arithmetic. 733-751 - Baoluo Meng
Synthesis of Optimal Defenses for System Architecture Design Model in MaxSMT. 752-770 - Michal Konecný
Certified Computation of Nondeterministic Limits. 771-789 - Lieuwe Vinkhuijzen
The Power of Disjoint Support Decompositions in Decision Diagrams. 790-799 - Kenny Ballou
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
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.
last updated on 2024-11-21 20:18 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: