Verification and Validation Challenges in Space Systems Workshop

IEEE Space Mission Challenges for Information Technology / Space Computing Conference

Hilton Pasadena - Pasadena, California

About the Workshop

Both the avionics and software used in space missions are growing significantly more complex and the verification and validation (V&V) of these systems is growing more difficult and costly. There is a growing need for new approaches to V&V that meet the challenges of enabling flight certification in a timely and cost-effective manner. This workshop focuses on the verification and validation of software and hardware systems for space with emphasis on processes, engineering methodologies, and tools to enable space flight certification of these systems. There will be a special session focusing on the transition to multi-core architectures such as the High-Performance Space Computer (HPSC) in space flight applications and the V&V challenges that arise from employing very complex processors that favor average case performance over deterministic behavior.

Workshop Format

The workshop will have a mix of both invited speakers and reviewed papers. The reviewed papers will appear in the SMC-IT/SCC conference proceedings.

Invited Speakers

Speaker: Dr. Joseph Kiniry, CEO & Chief Scientist Sigil Logic

Abstract:

In this talk I will describe HOARDE — the Hierarchical Orchestration of Autonomous Rigorous Digital Entities — built by my company, Sigil Logic, since our founding in September, 2025. HOARDE realizes what we call the NINJA methodology (Non-Intrusive Judicious Assurance): rigorous engineering with applied formal methods, made accessible to every engineering team through AI agents. HOARDE works alongside engineers to autonomously create high-assurance systems, generate formal specifications, find gaps in requirements and design, and prepare artifacts for certification and accreditation. It augments a team with what feels like dozens of coworkers who understand rigorous engineering, model-based development, and formal verification.

A critical design constraint is that HOARDE can operate entirely on local models — no cryptographic designs, proprietary specifications, or mission-critical system descriptions are ever sent to cloud-hosted LLMs in a local-only deployment. This privacy-preserving architecture makes HOARDE suitable for sensitive and classified work. HOARDE's agents maintain an unbroken refinement chain — from domain model through requirements, architecture, design, implementation, tests, and formal evidence — with full bidirectional traceability. Every operation produces verifiable evidence with recorded provenance. This is not ad hoc AI-assisted development; it is a principled, reproducible methodology enforced by the agents themselves. While creating rigorous specifications and models, HOARDE also trains engineers in the formal languages and tools working behind the scenes, producing a learning loop that has demonstrated substantial efficiency improvements in our internal case studies and meaningfully up-skills as they work.

Bio:

Dr. Joseph Kiniry is a leading expert in rigorous engineering with applied formal methods and model-based engineering — the practical discipline he calls the NINJA methodology. He is co-founder, CEO, and Chief Scientist of Sigil Logic, which builds AI-driven formal-methods and model-based-engineering tools that integrate into existing engineering workflows to make correct, secure, high-assurance hardware, firmware, and software achievable at scale — backed by machine-checkable evidence rather than hope. He is also CEO and Chief Scientist of Free & Fair, a Galois spin-out delivering high-assurance elections technologies using the same techniques applied to U.S. national-security problems. For twelve years he was a Principal Scientist at Galois in the Rigorous Digital Engineering area, where he ran more than thirty projects worth over $100M combined. Before Galois he was a Full Professor and Head of the Software Engineering section at the Technical University of Denmark, after permanent positions at universities in Denmark, Ireland, and the Netherlands. A Senior Member of the IEEE and ACM, he has served on more than one hundred program committees and keynoted dozens of international conferences, has advised the Dutch, Irish, Danish, and U.S. governments, and holds five advanced degrees including a Ph.D. from Caltech.

Speaker: Joel Sherrill, Chief Scientist Oar Corporation

Abstract:

Abstract: RTEMS is a free, open source, real-time operating system that supports multiple standards and includes support for multiple space-hardened microprocessors. RTEMS is commonly used in space applications and has a long history of successful deployment in critical applications. This presentation focuses on recent additions and improvements to RTEMS and its supporting Ecosystem that will be of interest to the flight software community. Key elements of the RTEMS Roadmap that the community should be aware of will be highlighted and the assurance challenges.

Bio:

Dr. Sherrill is Chief Scientist for OAR Corporation with over forty years of experience in the design, development, and fielding of real-time embedded applications in a variety of commercial, research, and military domains. Dr. Sherrill has been an active member of the free software community for over thirty years. As a principal author and current maintainer of the open-source real-time operating system RTEMS, he has been deeply involved in many RTEMS related efforts. He is a founding member of the Steering Committee for the Free Software Foundation’s GNU Compiler Collection and served as a board member of the Network Time Foundation.

Dr. Sherrill is currently serving as a representative for the U.S. Army to the Open Group Future Airborne Capability Environment (FACE™) Consortium and serves as lead for the Operating System Segment Subcommittee.

Dr. Sherrill earned a BS in Computer Science at the University of Tennessee at Chattanooga and MS and PhD degrees in Computer Science from the University of Alabama in Huntsville.

Speaker: Bill Dillard, Technology Strategy Lead for Advanced R&D Programs Microchip Technology Aerospace and Defense Group

Abstract:

Supporting Certified Avionics in the Multicore Era

The aviation industry’s move toward multicore processors is driven by necessity. Increasingly complex avionics workloads, higher levels of autonomy, sensor fusion, and advanced communications demand computational density that single‑core architectures can no longer provide within acceptable size, weight, and power (SWaP) envelopes. Multicore processors offer a compelling answer, but they also introduce a fundamental certification risk: how to demonstrate deterministic behavior in the presence of shared resources.

This challenge is now well understood by regulators and system designers alike. CAST‑32A reframes this risk by introducing the concept of interference channels and requiring applicants to identify, bound, and mitigate them as part of the system safety case. FAA Advisory Circular AC 20‑193 and its EASA equivalent AC AMC 20-193, builds on this foundation, providing practical guidance on acceptable means of compliance, including architectural mitigation, robust partitioning strategies, and verification evidence proportional to Design Assurance Level (DAL). In effect, certification authorities are no longer satisfied with software partitioning alone. Determinism must be demonstrated across hardware, firmware, and software layers, and that has profound implications for processor selection and platform architecture.

Bio:

Bill Dillard is a member of the Aerospace and Defense Group at Microchip Technology, where he serves as Technology Strategy Lead for Advanced R&D Programs. In this role, he aligns cross–business unit capabilities with emerging government and industry initiatives, defining strategy for next-generation aerospace and defense systems.

His work has centered on semiconductor technologies for demanding environments, with published research spanning low-temperature behavior of silicon devices, high-temperature silicon carbide (SiC) applications, and digital control of power electronics systems. Prior to joining Microchip, Bill spent 18 years in the aviation industry in roles spanning product development, sales, and government-funded programs. His work included microelectronics, inertial systems, radiation effects in semiconductors, and the design and production of FAA-certified avionics systems.

 

Bill holds a Bachelor of Science and a Master of Science in Electrical Engineering from Auburn University.

Accepted Papers

— Viktor Zagrebin, “Adaptive Orbital Engine: Continuous V&V for Degrading COTS AI Processors in LEO and VLEO”

— Ian Land, Ching Hu and Kristi Hoffman, “A V&V Framework for Assured AI/ML Integration in Space Avionics”

— Leonidas Kosmidis, Matina Maria Trompouki, Marc Solé i Bonet, Jannis Wolf, Eric Rufart, Pau Lopez Castillon, Ivan Rodiguez-Ferrandez, Dimitris Aspetakis and Guillermo Vidal, “Validation and Verification of Complex Flight Software on Complex Hardware: Lessons Learnt from Aerospace Research Projects”

Paper Submission Guidelines

• Paper Submissions We welcome full papers, which should adhere to the IEEE formatting guidelines, available here, and require a verbal presentation. Please submit your draft paper for review by the deadline listed below; paper acceptance notification will follow peer and program committee review. Alternatively, an abstract can be submitted in lieu of a draft paper. The final “camera-ready” paper must be submitted by the deadline listed below.
• Page Limit Full papers should not exceed six pages, excluding references.
• Publication All accepted papers will be published in the IEEE conference proceedings, indexed with the IEEE Xplore database. Note that IEEE has a “Podium and Publish” policy for conferences, which means that no manuscript will be published in IEEE Xplore without first being presented at the conference.

Important Dates Extended

• Saturday, May 23 Saturday, June 8. Submission deadline for papers to be in proceedings
• Monday, June 15. Abstracts for presentation only.
• Saturday, June 13 Thursday June 18. Notification of acceptance of papers and presentations
• Saturday, June 27. Wednesday, July 1. Final Copy of papers for proceedings due.

Topics of Interest

• Automating V&V processes
• V&V of multicore software
• V&V of AI enabled systems
• What to do when the data is the algorithm
• Applying AI in the V&V lifecycle
• V&V of embedded systems
• V&V of robotics
• Automated reasoning
• V&V of fault-tolerant systems
• Assurance of autonomous systems
• Formal and informal requirements in V&V
• Use cases of V&V on space systems
• Software testing

Chairs

• Alwyn E. Goodloe (NASA Langley Research Center)
• Scott Tashakkor (NASA Marshall Space Flight Center)

Program Committee

• Bjorn Andersson (SEI)
• Laura Humphrey (NASA)
• Michael Monaghan (NASA)
• Alessardro Pinto (JPL)
• Jan Sommer (DRL)
• Tim Wang (RTX)

Call for Papers

See call for papers