Invited Keynotes
Formal Methods for Trusted Space Autonomy: Boon or Bane
An Essence of Domain Engineering - A Basis for Trustworthy Aeronautics and Space Software
Concept Design Moves
Automating Program Transformation with Coccinelle
The Prusti Project: Formal Verification for Rust
Summers Reachability Analysis for Cyber-Physical Systems: Are we there yet
Regular Submissions
Towards Better Test Coverage: Merging Unit Tests for Autonomous Systems
Quantification of Battery Depletion Risk Made Efficient
Hierarchical Contract-based Synthesis for Assurance Cases
Verified Probabilistic Policies for Deep Reinforcement Learning
NNLander-VeriF: A Neural Network Formal Verification Framework for Vision-Based Autonomous Aircraft Landing
The Black-Box Simplex Architecture for Runtime Assurance of Autonomous CPS
Case Studies for Computing Density of Reachable States for Safe Autonomous Motion Planning
Towards Refactoring FRETish Requirements
Neural Network Compression of ACAS Xu Early Prototype is Unsafe: Closed-Loop Verification through Quantized State Backreachability
ZoPE: A Fast Optimizer for ReLU Networks with Low-Dimensional Inputs
Permutation Invariance of Deep Neural Networks with ReLUs
Configurable Benchmarks for C Model Checkers
AssumeGuarantee Reasoning with Scheduled Components
Stateful Black-Box Fuzzing of Bluetooth Devices Using Automata Learning
From Verified Scala to STIX File System Embedded Code using Stainless
On the Termination of Borrow Checking in Featherweight Rust
Programming Than Programming: Teaching Formal Methods in a Software Engineering Programme
Zone Extrapolations in Parametric Timed Automata
Exemplifying Parametric Timed Specifications over Signals with Bounded Behavior
Timed Automata Learning via SMT Solving
Asynchronous Composition of Local Interface LTL Properties
Elucidation and Analysis of Specification Patterns in Aerospace System Telemetry
Robust Computation Tree Logic
On the-Fly Model Checking with Neural MCTS
Checking and Test Generation for Comprehensive Verification
Operational Annotations: a New Method for Sequential Program Verification
Byzantine Fault Tolerant Consensus in Agda
DSV: Disassembly Soundness Validation without Assuming a Ground Truth
Probabilistic Hyperproperties with Rewards
Hypercontracts
Monitorability of Expressive Verdicts
BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees
Approximate Translation from Floating-Point to Real-Interval Arithmetic
Synthesis of Optimal Defenses for System Architecture Design Model in MaxSMT
Certified Computation of Nondeterministic Limits
The Power of Disjoint Support Decompositions in Decision Diagrams
Incremental Transitive Closure for Zonal Abstract Domain
Proof Mate: an Interactive Proof Helper for PVS
Runtime Verification Triggers
Real-time, Autonomous Fault Recovery on the CySat-I.