Invited Speakers
Supply Chain Attacks: If the Weakest Link Breaks the Chain
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.
Global Trajectory Optimization Competition (GTOC): The Case of GTOC12
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.
Verified Explanations of Neural Networks
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.
From Requirements to the Verification of Stochastic Systems
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.
Bridging Optimization and Onboard Decision-Making: Automated Reasoning in Space Systems and Logistics
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.