Symposium on AI-assisted Formal Specifications at ICSE 2025
Who's Atlas Computing?
Atlas Computing is a non-profit helping to empower human control over risky AI capabilities. https://atlascomputing.org/
What's this about?
As AI increasingly automates design and implementation of software, we need trust that the generated software does what humans intend. As AI-generated solutions grow increasingly abundant and complex, our challenge grows.
The mainstream test-and-review paradigm to software assurance will struggle to scale to AI-generated code. Automated verification techniques like property-based testing, model checking, and theorem proving provide huge benefits over manual techniques to system assurance, code synthesis efficiency, and scalable review. However, these techniques rely on formal specifications. This increases the importance of authoring formal specifications and validating that they match intent. We hypothesize that it is critical to empower engineers and subject matter experts to generate and review formal specification: software requirements stated in an objective, machine-readable way.
What's in for me?
This Symposium is designed to bring together the most relevant voices and projects in AI-assisted formal specs and provide everyone with an update on the cross-functional efforts between academia and industry.
What should I bring?
Your research, a friend or colleague, and lots of curiosity and passion for the topic.