ABSTRACT. Verified explanations offer a principled way to explain neural network decisions by grounding explainability in formally verified robustness, thereby addressing the inherently black-box nature of these models. We propose two complementary notions of verified explanations. The first is defined over the input space of neural networks, where we introduce hierarchical explanations, termed verifier-optimal robust explanations. These explanations explicitly account for the incompleteness of neural network verifiers, ensuring optimality with respect to the guarantees that can be formally established. The second notion is defined over the network’s internal (latent) representations, capturing explanations in terms of the model’s inner computations. We present novel efficient algorithms to compute both forms of explanations, and showcase their scalability and meaningfulness in practice.

ABSTRACT. Machine learning (ML) is increasingly adopted in space missions to enable on-board autonomy under strict constraints on power, compute, and communication. However, the deployment of ML in mission-critical satellite subsystems remains limited by the lack of rigorous verification and validation (V&V) approaches that can provide trust in model behavior under specified conditions. This work presents the study of the formal verification methods for satellite telemetry anomaly detection on the OPS-SAT mission benchmark. Specifically, we formally verify critical properties, scenarios, and robustness of the trained fully-connected neural network model using the pyNeVer and αβCrown libraries. We also discuss key benefits, challenges and limitations pertaining to the potential on-board deployment of formal verification methods in this use case. This integrated approach supports both pre-flight qualification and in-flight monitoring of ML components, aligning with emerging standards for ML assurance in aerospace systems.

ABSTRACT. Creating meaningful interpretations for black-box machine learning models involves balancing two often conflicting objectives: ac- curacy and explainability. Exploring the trade-off between these objec- tives is essential for developing trustworthy interpretations. While many techniques for multi-objective interpretation synthesis have been devel- oped, they typically lack formal guarantees on the Pareto-optimality of the results. Methods that do provide such guarantees, on the other hand, often face severe scalability limitations when exploring the Pareto- optimal space. To address this, we develop a framework based on local optimality guarantees that enables more scalable synthesis of interpre- tations. Specifically, we consider the problem of synthesizing a set of Pareto-optimal interpretations with local optimality guarantees, within the immediate neighborhood of each solution. Our approach begins with a multi-objective learning or search technique, such as Multi-Objective Monte Carlo Tree Search, to generate a best-effort set of Pareto-optimal candidates with respect to accuracy and explainability. We then verify local optimality for each candidate as a Boolean satisfiability problem, which we solve using a SAT solver. We demonstrate the efficacy of our approach on a set of benchmarks, comparing it against previous methods for exploring the Pareto-optimal front of interpretations. In particular, we show that our approach yields interpretations that closely match those synthesized by methods offering global guarantees. This work was accepted at ATVA 2025. We believe that our work and approach potentially has applications in autonomous space vehicles that use complex ML models.

ABSTRACT. We perform uncertainty propagation on an event manifold for Guidance & Control Networks (G&CNETs), aiming to enhance the certification tools for neural networks in this field. This work utilizes three previously solved optimal control problems with varying levels of dynamics nonlinearity and event manifold complexity. The G&CNETs are trained to represent the optimal control policies of a time-optimal interplanetary transfer, a mass-optimal landing on an asteroid and energy-optimal drone racing, respectively. For each of these problems, we describe analytically the terminal conditions on an event manifold with respect to initial state uncertainties. Crucially, this expansion does not depend on time but solely on the initial conditions of the system, thereby making it possible to study the robustness of the G&CNET at any specific stage of a mission defined by the event manifold. Once this analytical expression is found, we provide confidence bounds by applying the Cauchy-Hadamard theorem and perform uncertainty propagation using moment generating functions. While Monte Carlo-based (MC) methods can yield the results we present, this work is driven by the recognition that MC simulations alone may be insufficient for future certification of neural networks in guidance and control applications.

ABSTRACT. Complex space systems, such as those deployed in orbital or deep-space environments, are increasingly reliant on the seamless integration of heterogeneous components operating in harsh, unpredictable conditions. While the necessary system requirements are usually extracted from multiple stakeholders, norms, and regulations in natural language, this approach often leads to dangerous ambiguities. Formal languages offer a rigorous means of expressing these requirements unambiguously, while enabling the detection of realizability issues and inconsistencies. In uncertain environments such as in space, stochastic modeling of subsystems is preferred to reason about the probability of a requirement holding or to estimate expected operational costs. In this talk, I present two tools for addressing these challenges: NASA’s FRET for eliciting deterministic and probabilistic requirements from structured natural language, and ULTIMATE for verifying stochastic world-models. We will end with a discussion on how these tools can be applied to complex space systems to bridge the gap between high-level requirements and rigorous, automated formal system verification.

ABSTRACT. The Plan Execution Interchange Language (PLEXIL) is an event-driven synchronous language developed by NASA to support autonomous spacecraft operations. Due to the safety- and mission-critical applications of PLEXIL, its semantics has been formalized and key properties of the language have been formally verified. Two of the properties explored in the formalization are operational determinism, which states that the only source of non-determinism in a PLEXIL execution is the external environment, and run-to-completion, which states that under well-defined assumptions, external events trigger a chain of internal computations that eventually terminate. This paper presents an overview of the formal semantics of the current version of the language, PLEXIL 6.

ABSTRACT. Observation planning is the task of scheduling the operations of a satellite constellation to take pictures of a set of regions of interest and sending these observations down to Earth. With large constellations, uncertain observation conditions, e.g. due to clouds, and limited availability of downstream capacity, it becomes increasingly hard to coordinate the operations. We address the setting where satellites have limited memory, and pictures need to be sent through the constellation to a satellite that can transmit them to a ground station. A key challenge in this problem is the highly dynamic environment, which requires a robust planning system that can quickly adapt to changes. We propose a framework based on facet reasoning, which, unlike traditional planners that provide a single fixed solution, allows for dynamic updates to the current solution without replanning from scratch. We show empirically that facets offer a scalable approach for constellation planning and illustrate the robustness in a case study.

ABSTRACT. Driven by the surmounting interest for dedicated infrastructure in cislunar space, this work considers the satellite constellation design for cislunar space situational awareness (CSSA). We propose a mixed-integer linear programming (MILP)-based formulation that simultaneously tackles the constellation design and sensor-tasking subproblems surrounding CSSA. Our approach generates constellation designs that provide coverage with considerations for the field of view of observers. We propose a time-expanded p-median problem (TE-p-MP) that considers the optimal placement of p space-based observers into discretized locations based on orbital slots along libration point orbits, simultaneously with observer pointing directions across discretized time. We further develop a Lagrangian method for the TE-p -MP, where a relaxed problem with an analytical solution is derived, and customized heuristics leveraging the orbital structure of candidate observer locations are devised. The performance of the proposed formulation is demonstrated with several case studies for CSSA constellations monitoring the cislunar Cone of Shame and a periodic time-varying transit window for low-energy transfers located in the Earth–Moon L2 neck region. The proposed problem formulation, along with the Lagrangian method, is demonstrated to enable a fast assessment of near-optimal CSSA constellations, equipping decision-makers with a critical technique for exploring the design trade space.

ABSTRACT. The Global Trajectory Optimization Competition (GTOC) is an international challenge in space mission design that formulates realistic, large-scale optimization problems and evaluates solutions through transparent mathematical scoring rules. This talk presents the structure and philosophy of GTOC using the 12th edition (GTOC12) as a case study. GTOC12 focused on asteroid mining, with the objective of maximizing the total mass of resources returned to Earth. Participants were required to design trajectories for multiple spacecraft performing asteroid rendezvous, resource extraction, and return missions under low-thrust propulsion constraints. The problem combined continuous optimal control with discrete combinatorial decision-making, including spacecraft allocation, target selection, sequencing, and timing. GTOC12 illustrates how future mission design integrates astrodynamics, optimization, and systems-level planning.

ABSTRACT. Space logistics and mission planning are becoming increasingly critical as humankind expands its presence in space. While simulation and analysis tools such as SpaceNet have been widely used to explore feasible architectures, their limited optimization capabilities make it difficult to fully avoid the cost of extensive trade space exploration. This paper presents a new open-source optimization toolbox for space mission planning, developed to automatically formulate and solve or find feasible solutions to mixed-integer nonlinear programs (MINLPs) that integrate discreteness of mission profiles and nonlinearity of systems design. The toolbox is designed for accessibility: users specify mission requirements and parameters, after which the corresponding optimization problem is generated and addressed by a solution approach of the user's choice, including state-of-the-art solvers and built-in heuristic algorithms. Current capabilities include integrated space mission planning and spacecraft design, support for both commercial and open-source mixed-integer solver options, and initial visualization of optimized network flows. The planned extensions focus on interactive visualization, expanded mission domains beyond the Earth–Moon system, and surface logistics integration. This rigorous yet accessible optimization toolbox aims to enable more efficient and optimal mission design processes to support future space exploration.

ABSTRACT. There are a number of types of space mission concepts that feature a single spacecraft visiting multiple targets through its mission. Such “tour” missions are commonly modelled as travelling-salesman problems (TSPs). However, the typical TSP modelling methods are complicated by the fact that the “customers” – the satellites that require servicing, for example – are in orbit, rather than stationary. Previous works resolve this issue either by representing entire orbits as single nodes in the salesman’s – for example, the servicer satellite’s - route, or by expanding orbits into multiple discrete time steps. Both of these methods therefore lose some fidelity in the time dimension, and consequently must make worst-case assumptions about the time-dependent cost of moving between nodes in order to maintain the feasibility of solutions. These worst-case assumptions can be inherently avoided by maintaining the time dimension of the problem as a continuous quantity, as opposed to constructing discrete time windows. Therefore, this paper constructs the Keplerian travelling salesman problem as a time-dependent travelling salesman problem and implements a dynamic programming approach to finding orbital tour schedules with exact, continuous time solutions. We present preliminary results and make comparisons with a state-of-the-art integer programming method.

ABSTRACT. Target selection for large-scale space survey missions requires selecting a scientifically valuable subset from a much larger pool of available targets. This represents a high-stakes combinatorial optimisation problem, since the final sample directly shapes the scientific return of the mission. Current operational approaches mainly rely on heuristic stratified sampling over low-dimensional parameter subspaces. While this paradigm captures key quantities of interest to astronomers, it becomes increasingly limited as the dimensionality and complexity of the planetary feature space grow. More importantly, there is currently no formal evaluation framework for comparing target-selection strategies against scientifically grounded criteria, leaving mission planners without principled tools for assessing representativeness or survey leverage. This problem is particularly relevant for ESA's Ariel mission, which aims to observe approximately 1,000 exoplanets selected from a much larger Mission Candidate Sample (MCS). Ariel will therefore be used in this work as a case study for developing and evaluating target-selection strategies. We propose a multi-objective subset selection framework that formalises target selection as the simultaneous optimisation of three core objectives: distributional similarity to the full candidate catalogue, quantified via the Wasserstein distance; internal subset diversity, maximised over the planetary feature space; and scheduling practicality, subject to mission lifetime and transit window constraints. A key contribution is the evaluation protocol itself, a fair, metric-grounded benchmarking arena for comparing arbitrary selection strategies, which the community currently lacks.

ABSTRACT. Modern computer systems consist of a large number of components that are developed by third parties and later integrated into the larger system. This reliance on externally developed modules creates a significant risk of supply chain attacks, in which some of the components are intentionally manipulated to disrupt or compromise the functionality of the overall system. A related challenge arises in federated learning, where individual participants may provide manipulated or malicious training data in order to influence the resulting model. In this talk, we first provide an overview of the risks posed by such attacks. We then present several countermeasures developed for security-critical cryptographic systems that leverage formal verification techniques to ensure robustness even in the presence of potentially compromised components. Finally, we discuss how these approaches can be adapted and applied to space systems, where reliability and security are particularly critical.

ABSTRACT. Modern space logistics systems increasingly rely on autonomous decision-making across multiple layers, from mission-level planning to onboard control and fault management. While these capabilities are often developed under different paradigms—such as planning, numerical optimization, and rule-based logic—they can be viewed through a unified lens of “automated reasoning under constraints.” This talk presents an industry perspective on how real-world space systems already implement such reasoning across a few layers such as: mission planning, continuous optimization for trajectory and control, and onboard fault detection and recovery logic. Drawing on experience from lunar mission design and operations, the talk highlights how these layers interact in practice, the limitations of current approaches, and opportunities to bridge them with advances in automated reasoning. The aim is to foster dialogue between the space and automatic reasoning communities toward more integrated and self-sustainable space logistics architectures.