HCSS 2025
Date: May 12, 2025 7:00 am – May 14, 2025 3:00 pm
Location: Annapolis, MD
Introduction
The twenty-fifth annual High Confidence Software and Systems (HCSS) Conference will be held May 12-14, 2025, at the Historic Inns of Annapolis in Annapolis, Maryland. We solicit proposals to present talks at the conference.
Background
Our security, safety, privacy, and well-being increasingly depend upon the correctness, reliability, resilience, and integrity of software-intensive systems of all kinds, including cyber-physical systems (CPS). These systems must be capable of interacting correctly, safely, and securely with humans, with diverse other systems, and with the physical world even as they operate in changing, difficult-to-predict, and possibly malicious environments. New foundations in science, technology, and methodologies continue to be needed. Moreover, these methods and tools must be transitioned into mainstream use to build and assure these systems—and to move towards more effective models for acceptance and certification.
Conference Scope, Goals, and Vision
The High Confidence Software and Systems (HCSS) Conference draws together researchers, practitioners, and management leaders from government, universities, non-profits, and industry. The conference provides a forum for dialogue centered upon the development of scientific foundations for the assured engineering of software-intensive complex computing systems and the transition of science into practice. The technical emphasis of the HCSS conference is on mathematically-based tools and techniques, scientific foundations supporting evidence creation, systems assurance, and security. The HCSS vision is one of engaging and growing a community—including researchers and skilled practitioners—that is focused around the creation of dependable systems that are capable, efficient, and responsive; that can work in dangerous or inaccessible environments; that can support large-scale, distributed coordination; that augment human capabilities; that can advance the mission of national security; and that enhance quality of life, safety, and security.
Conference Themes
We invite submissions on any topic related to high-confidence software and systems that aligns with the conference scope and goals listed above. In addition, the 2025 HCSS Conference will highlight the following themes:
AI and Models in the Software Development Lifecycle
Model-Based Software Development is based on the creation of rich models that describe multiple aspects of a system, well before any code is written or libraries selected. Good models enable the discovery of unexpected system interactions and potential failure modes early in the design process, as well as providing accurate descriptions of the required functionality. Unfortunately, there seems to be a dearth of well-developed principles for connecting such models to the code as it gets written, built, and maintained. All too often, software teams will be given little more than architectural diagrams derived from the modeling process as a guide for how to proceed. With no automated bridge to close the loop between the code and modeling, the two efforts start to diverge, and much of the potential benefit of the modeling is lost.
A parallel and rapidly emerging trend is the application of AI/ML techniques in software development and their use as “assistants” to code developers. Github’s Copilot, GPT-Code-Clippy, Starcoder, and Meta Code Llama are just a few examples of systems based on Large Language Models (LLM) that are increasingly being used by developers today. However, as we observe above, software development is much more than coding and there are opportunities to use AI in other phases of the software development life cycle. Today’s agile software development practices and aggressive production schedules continuously pressure developers to increase their productivity, while increasing quality and the dependability of software, especially for mission- or safety-critical applications.
These trends raise several key questions that this topic will explore:
- How can AI support and enhance the entire software development lifecycle?
- How can AI close the loop between models and code?
- What roles do AI, models, and human developers play in a comprehensive software development process?
- How does AI affect software quality and dependability?
- How can model-based approaches assess para-functional properties in AI-augmented processes?
- What are the risks and benefits of AI-augmented development?
Topics of interest span the application of AI and models in all phases of the software development lifecycle:
- Requirements & Architecture Development: Reviewing documents for clarity, consistency, and compliance with MBSE standards.
- Detailed Design: Summarizing complex technical information into concise reports for stakeholders. Automatically generating model diagrams.
- Models to Code: Principles and methods to connect code and their models so that the two worlds can stay synchronized over time – this includes theoretical approaches, practical tools, and experience reports.
- Implementation, Test & Verification: Identifying best practices and design patterns for implementing specific system functionalities. Generating code / hardware design for faster implementation and enhanced reuse.
- System Verification & Validation: Searching vast repositories of engineering data and past projects for hazard analysis and validation.
- Operation & Maintenance: Answering questions about the system model improving transparency.
- Communication & Collaboration: Intelligent assistants helping engineers translate technical documents between teams
Formal Verification of AI/ML Systems
We are seeing rapid improvements in techniques and tools based on formal methods that can rigorously verify aspects of machine learning (ML) models and systems. These tools successfully verify a wide variety of learned models and systems for increasingly complex applications, as well as learning-based methods for generating them. Less than a decade ago, the only methods for ML verification relied on "black box" testing and statistical methods to characterize behavior and performance. State-of-the-art tools combining SMT solvers, linear programming, and other techniques can now reason about complex deep neural networks with different architectures and formats. Parallelization and algorithmic improvements have increased scalability to networks approaching millions of parameters.
As machine learning continues to find its way into many more applications with safety-, mission-, and security-critical requirements, the comprehensive guarantees possible with formal methods-based approaches will become increasingly necessary. Formal methods tools are verifying requirements and establishing robustness, stability, and generalization properties of ML-based systems, and can now do so with greater confidence than traditional data-driven statistical approaches requiring infeasibly large datasets.
Topics of interest include:
- Formal methods for verification and validation of ML-based systems including DNNs
- Connecting different formal techniques to enable explainability
- Scalable strategies for formal verification of ML-based systems, especially as applied to vision/perception systems
- Formal methods approaches for verification of systems trained using reinforcement learning or unsupervised learning
- Competitions and other experiments comparing tool performance
Formalizing Pure Math
We have entered a new area of using formal reasoning in the pursuit of pure mathematics. Articles in Nature, Scientific American, New York Times, and Wired this past year discuss how professional mathematicians are discovering the benefits of formalizing mathematics. Fields Medalists are popularizing the use of theorem-proving to formalize results. Mathematics has several challenges in formalization, including building up suitable domain-specific libraries, teaching mathematicians how to use (sometimes arcane) theorem provers, and managing large-scale proofs. However, it benefits work in pure math just as it does in software and hardware, by helping clarify thought and prevent errors in reasoning.
In addition, theorem provers have recently been revisited as a way to reduce hallucination in LLMs when applied to mathematical reasoning, Google’s silver medal in the 2024 Intl. Math Olympiad competition combines LLMs and a theorem prover. We expect work combining LLMs and theorem-proving to rapidly advance in assisting pure mathematicians.
We welcome contributions that relate to these topics and applications, such as:
- Leveraging formal reasoning in mathematics education.
- Recent results in formalizing or automating mathematics.
- Lessons-learned and experience reports in formalizing various math domains and building pure math libraries.
- Combining LLMs with formal reasoning in pure math.
- Engineering and social challenges in proof maintenance and collaboration in mathematics.
- Peer review & social acceptance in mathematical communities of formal reasoning.
- Interoperability with more traditional software systems for pure math (e.g., Mathematica, MATLAB, etc.).
Novel Automated Reasoning Applications
Growing maturity of automated reasoning tools such as theorem provers and SMT solvers has led to ever increasing use of software-modeling for system improvement. Computer science methods and mathematical rigor are finding applications in new and sometimes surprising ways. In diverse domains ranging from critical social system norms to financial markets, software-like artifacts model key domain behaviors and automated reasoning tools establish important properties. Such artifacts will play an increasingly critical role in system design, implementation, verification and certification.
HCSS seeks abstracts that describe how automated reasoning supports modeling and guarantees beyond traditional hardware and software correctness. Potential domains include (but are not limited to)
- Resilience of social systems under stress,
- Financial market regulatory compliance and resilience,
- Computational contracts and law,
- Mixed reality systems safety,
- Database query integration automation,
- Structured test coverage comprehensiveness,
- Automated safety analysis, and
- Predictive models of cyber-social interactions.
Technical advances or use reports where tool-supported mathematical rigor and automated reasoning improves reliability, increases resilience, or provides a new formal modeling approach are of particular interest.
Conference Presentations
The conference program features invited speakers, panel discussions, poster presentations, and a technical track of contributed talks.
Technical Track Presentations
The technical track features two kinds of talks:
Experience reports. These talks inform participants about how emerging HCSS and CPS techniques play out in real-world applications, focusing especially on lessons learned and insights gained. Although experience reports do not have to be highly technical, they should emphasize substantive and comprehensive reflection, building on data and direct experience. Experience reports focus on topics such as transitioning science into practice, architecture and requirements, use of advanced languages and tools, evaluation and assessment, team practice and tooling, supply-chain issues, etc.
Technical talks. These talks highlight state-of-the-art techniques and methods for high-confidence software systems with an emphasis on how those techniques and methods can be used in practice. Presenters of these talks should strive to make their material accessible to the broader HCSS community even as they discuss deep technical results in areas as diverse as concurrency analysis, hybrid reasoning approaches, theorem proving, separation logic, synthesis, analytics, various modeling techniques, etc.
If you are interested in offering a talk—or nominating someone else to be invited to do so—please upload an abstract of one page or less for your proposed talk or a one paragraph description of your nominee’s proposed talk by January 13, 2025 to https://sos-vo.org/group/hcss_conference/cfp/2025-submit. Abstracts and nomination paragraphs should clearly indicate why the talk would be relevant to HCSS and which, if any, conference themes the talk would address. Notifications of accepted presentations will be made by February 17, 2025.
Further instructions for electronically submitting print-ready abstracts and final slide presentations will be provided in the acceptance notification messages. Abstracts of accepted presentations will be published on the HCSS Conference website.
Co-located Meetings
We are pleased to once again welcome the co-location of the Trusted Computing Center of Excellence™ (TCCoE) Summit. The mission of the TCCoE is to lower barriers to adoption and facilitate the principled development and deployment of trustworthy systems. The TCCoE, originally focused on facilitating the adoption of the seL4 kernel in critical defense systems. Recently, the TCCoE has broadened their mission to promote the adoption and deployment of formally verified software (including seL4) in defense applications whose mission requires the highest levels in assurance. The annual TCCoE Summit brings together like-minded individuals from Government, Industry, and Academia to learn of relevant developments, make connections, and work toward the TCCoE’s goals. This year’s summit will leverage synergies with the High Confidence Software and Systems Conference. The overlap between the technologies of interest of these two events and their complementary missions will provide interested attendees a tremendous experience. The TCCoE Summit will be held on May 12-14, 2025.
The Software Certification Consortium (SCC) meeting will again be co-located with HCSS. The meeting will run concurrently to the TCCoE Summit on May 12-14, 2025. The Software Certification Consortium is a group of researchers/practitioners who are interested in the development and certification of high integrity systems. SCC typically meets twice a year, and the themes of the meetings are designed to contribute to a long-term SCC work plan.
Important Dates
CfP Abstracts Due: January 13, 2025
Notification of Decisions: February 17, 2025
HCSS Conference: May 12-14, 2025
Co-located Meetings
TCCOE Summit: May 15-16, 2025
SCC Meeting: May 15-16, 2025
Planning Committee
Co-Chairs
Darren Cofer, Collins Aerospace
Sandeep Neema, Vanderbilt University
Steering Group
Perry Alexander, University of Kansas
June Andronick, Proofcraft
Kathleen Fisher, DARPA
John Hatcliff, Kansas State University
John Launchbury, Galois, Inc.
Patrick Lincoln, SRI International
Stephen Magill, Sonatype
Brad Martin, National Security Agency
Lee Pike, Amazon Web Services
Ray Richards, Leidos
Bill Scherlis, Carnegie Mellon University
Eric Smith, Kestrel Institute
Adam W, National Cyber Security Centre
Sean Weaver, DARPA
Matt Wilding, DARPA
Kristin Yvonne Rozier, Iowa State University
Organization
Katie Dey, Vanderbilt University
Sponsor Agency
NITRD HCSS Coordinating Group
Submitted by Regan Williams
on
Introduction
The twenty-fifth annual High Confidence Software and Systems (HCSS) Conference will be held May 12-14, 2025, at the Historic Inns of Annapolis in Annapolis, Maryland. We solicit proposals to present talks at the conference.
Background
Our security, safety, privacy, and well-being increasingly depend upon the correctness, reliability, resilience, and integrity of software-intensive systems of all kinds, including cyber-physical systems (CPS). These systems must be capable of interacting correctly, safely, and securely with humans, with diverse other systems, and with the physical world even as they operate in changing, difficult-to-predict, and possibly malicious environments. New foundations in science, technology, and methodologies continue to be needed. Moreover, these methods and tools must be transitioned into mainstream use to build and assure these systems—and to move towards more effective models for acceptance and certification.
Conference Scope, Goals, and Vision
The High Confidence Software and Systems (HCSS) Conference draws together researchers, practitioners, and management leaders from government, universities, non-profits, and industry. The conference provides a forum for dialogue centered upon the development of scientific foundations for the assured engineering of software-intensive complex computing systems and the transition of science into practice. The technical emphasis of the HCSS conference is on mathematically-based tools and techniques, scientific foundations supporting evidence creation, systems assurance, and security. The HCSS vision is one of engaging and growing a community—including researchers and skilled practitioners—that is focused around the creation of dependable systems that are capable, efficient, and responsive; that can work in dangerous or inaccessible environments; that can support large-scale, distributed coordination; that augment human capabilities; that can advance the mission of national security; and that enhance quality of life, safety, and security.
Conference Themes
We invite submissions on any topic related to high-confidence software and systems that aligns with the conference scope and goals listed above. In addition, the 2025 HCSS Conference will highlight the following themes:
AI and Models in the Software Development Lifecycle
Model-Based Software Development is based on the creation of rich models that describe multiple aspects of a system, well before any code is written or libraries selected. Good models enable the discovery of unexpected system interactions and potential failure modes early in the design process, as well as providing accurate descriptions of the required functionality. Unfortunately, there seems to be a dearth of well-developed principles for connecting such models to the code as it gets written, built, and maintained. All too often, software teams will be given little more than architectural diagrams derived from the modeling process as a guide for how to proceed. With no automated bridge to close the loop between the code and modeling, the two efforts start to diverge, and much of the potential benefit of the modeling is lost.
A parallel and rapidly emerging trend is the application of AI/ML techniques in software development and their use as “assistants” to code developers. Github’s Copilot, GPT-Code-Clippy, Starcoder, and Meta Code Llama are just a few examples of systems based on Large Language Models (LLM) that are increasingly being used by developers today. However, as we observe above, software development is much more than coding and there are opportunities to use AI in other phases of the software development life cycle. Today’s agile software development practices and aggressive production schedules continuously pressure developers to increase their productivity, while increasing quality and the dependability of software, especially for mission- or safety-critical applications.
These trends raise several key questions that this topic will explore:
- How can AI support and enhance the entire software development lifecycle?
- How can AI close the loop between models and code?
- What roles do AI, models, and human developers play in a comprehensive software development process?
- How does AI affect software quality and dependability?
- How can model-based approaches assess para-functional properties in AI-augmented processes?
- What are the risks and benefits of AI-augmented development?
Topics of interest span the application of AI and models in all phases of the software development lifecycle:
- Requirements & Architecture Development: Reviewing documents for clarity, consistency, and compliance with MBSE standards.
- Detailed Design: Summarizing complex technical information into concise reports for stakeholders. Automatically generating model diagrams.
- Models to Code: Principles and methods to connect code and their models so that the two worlds can stay synchronized over time – this includes theoretical approaches, practical tools, and experience reports.
- Implementation, Test & Verification: Identifying best practices and design patterns for implementing specific system functionalities. Generating code / hardware design for faster implementation and enhanced reuse.
- System Verification & Validation: Searching vast repositories of engineering data and past projects for hazard analysis and validation.
- Operation & Maintenance: Answering questions about the system model improving transparency.
- Communication & Collaboration: Intelligent assistants helping engineers translate technical documents between teams
Formal Verification of AI/ML Systems
We are seeing rapid improvements in techniques and tools based on formal methods that can rigorously verify aspects of machine learning (ML) models and systems. These tools successfully verify a wide variety of learned models and systems for increasingly complex applications, as well as learning-based methods for generating them. Less than a decade ago, the only methods for ML verification relied on "black box" testing and statistical methods to characterize behavior and performance. State-of-the-art tools combining SMT solvers, linear programming, and other techniques can now reason about complex deep neural networks with different architectures and formats. Parallelization and algorithmic improvements have increased scalability to networks approaching millions of parameters.
As machine learning continues to find its way into many more applications with safety-, mission-, and security-critical requirements, the comprehensive guarantees possible with formal methods-based approaches will become increasingly necessary. Formal methods tools are verifying requirements and establishing robustness, stability, and generalization properties of ML-based systems, and can now do so with greater confidence than traditional data-driven statistical approaches requiring infeasibly large datasets.
Topics of interest include:
- Formal methods for verification and validation of ML-based systems including DNNs
- Connecting different formal techniques to enable explainability
- Scalable strategies for formal verification of ML-based systems, especially as applied to vision/perception systems
- Formal methods approaches for verification of systems trained using reinforcement learning or unsupervised learning
- Competitions and other experiments comparing tool performance
Formalizing Pure Math
We have entered a new area of using formal reasoning in the pursuit of pure mathematics. Articles in Nature, Scientific American, New York Times, and Wired this past year discuss how professional mathematicians are discovering the benefits of formalizing mathematics. Fields Medalists are popularizing the use of theorem-proving to formalize results. Mathematics has several challenges in formalization, including building up suitable domain-specific libraries, teaching mathematicians how to use (sometimes arcane) theorem provers, and managing large-scale proofs. However, it benefits work in pure math just as it does in software and hardware, by helping clarify thought and prevent errors in reasoning.
In addition, theorem provers have recently been revisited as a way to reduce hallucination in LLMs when applied to mathematical reasoning, Google’s silver medal in the 2024 Intl. Math Olympiad competition combines LLMs and a theorem prover. We expect work combining LLMs and theorem-proving to rapidly advance in assisting pure mathematicians.
We welcome contributions that relate to these topics and applications, such as:
- Leveraging formal reasoning in mathematics education.
- Recent results in formalizing or automating mathematics.
- Lessons-learned and experience reports in formalizing various math domains and building pure math libraries.
- Combining LLMs with formal reasoning in pure math.
- Engineering and social challenges in proof maintenance and collaboration in mathematics.
- Peer review & social acceptance in mathematical communities of formal reasoning.
- Interoperability with more traditional software systems for pure math (e.g., Mathematica, MATLAB, etc.).
Novel Automated Reasoning Applications
Growing maturity of automated reasoning tools such as theorem provers and SMT solvers has led to ever increasing use of software-modeling for system improvement. Computer science methods and mathematical rigor are finding applications in new and sometimes surprising ways. In diverse domains ranging from critical social system norms to financial markets, software-like artifacts model key domain behaviors and automated reasoning tools establish important properties. Such artifacts will play an increasingly critical role in system design, implementation, verification and certification.
HCSS seeks abstracts that describe how automated reasoning supports modeling and guarantees beyond traditional hardware and software correctness. Potential domains include (but are not limited to)
- Resilience of social systems under stress,
- Financial market regulatory compliance and resilience,
- Computational contracts and law,
- Mixed reality systems safety,
- Database query integration automation,
- Structured test coverage comprehensiveness,
- Automated safety analysis, and
- Predictive models of cyber-social interactions.
Technical advances or use reports where tool-supported mathematical rigor and automated reasoning improves reliability, increases resilience, or provides a new formal modeling approach are of particular interest.
Conference Presentations
The conference program features invited speakers, panel discussions, poster presentations, and a technical track of contributed talks.
Technical Track Presentations
The technical track features two kinds of talks:
Experience reports. These talks inform participants about how emerging HCSS and CPS techniques play out in real-world applications, focusing especially on lessons learned and insights gained. Although experience reports do not have to be highly technical, they should emphasize substantive and comprehensive reflection, building on data and direct experience. Experience reports focus on topics such as transitioning science into practice, architecture and requirements, use of advanced languages and tools, evaluation and assessment, team practice and tooling, supply-chain issues, etc.
Technical talks. These talks highlight state-of-the-art techniques and methods for high-confidence software systems with an emphasis on how those techniques and methods can be used in practice. Presenters of these talks should strive to make their material accessible to the broader HCSS community even as they discuss deep technical results in areas as diverse as concurrency analysis, hybrid reasoning approaches, theorem proving, separation logic, synthesis, analytics, various modeling techniques, etc.
If you are interested in offering a talk—or nominating someone else to be invited to do so—please upload an abstract of one page or less for your proposed talk or a one paragraph description of your nominee’s proposed talk by January 13, 2025 to https://sos-vo.org/group/hcss_conference/cfp/2025-submit. Abstracts and nomination paragraphs should clearly indicate why the talk would be relevant to HCSS and which, if any, conference themes the talk would address. Notifications of accepted presentations will be made by February 17, 2025.
Further instructions for electronically submitting print-ready abstracts and final slide presentations will be provided in the acceptance notification messages. Abstracts of accepted presentations will be published on the HCSS Conference website.
Co-located Meetings
We are pleased to once again welcome the co-location of the Trusted Computing Center of Excellence™ (TCCoE) Summit. The mission of the TCCoE is to lower barriers to adoption and facilitate the principled development and deployment of trustworthy systems. The TCCoE, originally focused on facilitating the adoption of the seL4 kernel in critical defense systems. Recently, the TCCoE has broadened their mission to promote the adoption and deployment of formally verified software (including seL4) in defense applications whose mission requires the highest levels in assurance. The annual TCCoE Summit brings together like-minded individuals from Government, Industry, and Academia to learn of relevant developments, make connections, and work toward the TCCoE’s goals. This year’s summit will leverage synergies with the High Confidence Software and Systems Conference. The overlap between the technologies of interest of these two events and their complementary missions will provide interested attendees a tremendous experience. The TCCoE Summit will be held on May 12-14, 2025.
The Software Certification Consortium (SCC) meeting will again be co-located with HCSS. The meeting will run concurrently to the TCCoE Summit on May 12-14, 2025. The Software Certification Consortium is a group of researchers/practitioners who are interested in the development and certification of high integrity systems. SCC typically meets twice a year, and the themes of the meetings are designed to contribute to a long-term SCC work plan.
Important Dates
CfP Abstracts Due: January 13, 2025
Notification of Decisions: February 17, 2025
HCSS Conference: May 12-14, 2025
Co-located Meetings
TCCOE Summit: May 15-16, 2025
SCC Meeting: May 15-16, 2025
Planning Committee
Co-Chairs
Darren Cofer, Collins Aerospace
Sandeep Neema, Vanderbilt University
Steering Group
Perry Alexander, University of Kansas
June Andronick, Proofcraft
Kathleen Fisher, DARPA
John Hatcliff, Kansas State University
John Launchbury, Galois, Inc.
Patrick Lincoln, SRI International
Stephen Magill, Sonatype
Brad Martin, National Security Agency
Lee Pike, Amazon Web Services
Ray Richards, Leidos
Bill Scherlis, Carnegie Mellon University
Eric Smith, Kestrel Institute
Adam W, National Cyber Security Centre
Sean Weaver, DARPA
Matt Wilding, DARPA
Kristin Yvonne Rozier, Iowa State University
Organization
Katie Dey, Vanderbilt University
Sponsor Agency
NITRD HCSS Coordinating Group