Table of Contents

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