Welcome to the website of SpecOps 2026, the 1st International Workshop on Specification-Driven Development Life Cycle. SpecOps brings together researchers and practitioners from Software Engineering, Programming Languages, Formal Methods, and Artificial Intelligence, and aims to foster dialogue on how AI-powered tools and autonomous agents can transform specifications from static documentation into living, executable, and lifecycle-spanning drivers of modern software and AI system development.

The workshop will be held on October 6th and collocated with ISSTA at the Oakland Marriott City Centre hotel.

Keynote Speakers

We are delighted to announce two distinguished keynote speakers for SpecOps 2026, whose pioneering research spans software engineering, programming languages, formal methods, and AI-driven software development.

Shuvendu Lahiri

Title: Intent Formalization: Assessing the Quality of AI-Generated Formal Program Specifications

Abstract: Agentic AI systems can now produce fluent code, but the core question persists: does the code reflect the user’s actual intent? The long‑standing gap between informal natural‑language requirements and precise program behavior—the intent gap—is magnified by AI‑generated code. The path to reliability runs through intent formalization: automatically translating informal intent into checkable specifications, ranging from lightweight tests to symbolic specs and domain‑specific languages. As AI systems become creative at generating such specifications, the bottleneck shifts from writing specs to evaluating them. Since specifications lack an independent oracle, verifying that they truly capture user intent is difficult and user‑dependent.

We will discuss how this evaluation can be rigorous and largely automated. Using tests as a proxy oracle, we define metrics—soundness, completeness, and preciseness—to quantify how well a specification matches intent across both mainstream and verification‑aware languages. Research prototypes demonstrate feasibility: tests to resolve intent ambiguities (TiCoder), quality assessment of symbolic specs (nl2postcond, Dafny spec validation), training a formal specification model (AutoVerus), and automated specification repair via agentic proof automation (F*). This work defines a research agenda spanning AI, programming languages, formal methods, and HCI.

Bio: Shuvendu Lahiri is a Senior Principal Researcher in the RiSE group at Microsoft Research Redmond. He has worked on SMT solvers, formal specification and verification, software testing, and combining formal methods/testing with LLMs with techniques such as Intent Formalization. He holds a PhD from Carnegie Mellon University and BTech from IIT Kharagpur. His works have received best/distinguished paper awards from leading formal methods, programming languages and software engineering conferences, a test-of-time award from ICSE, and a CAV award for foundations of SMT solvers, an ACM SIGDA outstanding PhD dissertation award. He is an ACM Distinguished member.

Learn more about his work at: https://www.microsoft.com/en-us/research/people/shuvendu/

Corina S. Păsăreanu & Joe Rutland

Title: Bridging Requirements and Assurance: Neurosymbolic Autoformalization for C++ Verification and Requirements-Coverage Testing

Abstact: We describe a neurosymbolic approach for the autoformalization of natural-language requirements into machine-checkable specifications. Our approach combines neural language models with symbolic reasoning to translate informal requirements into a structured executable representation amenable to downstream symbolic execution. This formalization serves as the foundation for two complementary assurance activities: (1) verification and automated test case generation for C++ implementations, ensuring behavioral conformance to specified requirements; and (2) requirements-coverage-driven test generation, producing test suites that achieve traceability and coverage criteria demanded by certification standards. The approach provides an integrated path from specification to certified assurance, reducing manual formalization effort while improving consistency between verification artifacts and certification evidence.

Bio: Dr. Corina Pasareanu is an ACM and IEEE ASE Fellow working at Amazon PrimeAir and Carnegie Mellon University’s CyLab. A member of the inaugural ACM SIGSOFT Software Engineering Academy, her research focuses on model checking, symbolic execution, autonomy, and security. She has received multiple Test of Time and Most Influential Paper awards (including ICSE, ESEC/FSE, ASE, ISSTA, and ETAPS) and frequently serves as General or Program Chair for top-tier conferences like ICSE 2025, ISSTA 2020, ESEC/FSE 2018, CAV 2015 and ASE 2011.

Learn more about her work at: https://www.andrew.cmu.edu/user/pcorina/

Joe Rutland is a software engineer at Amazon Prime Air, Amazon’s drone delivery program, where he works on the development and verification of embedded software under DO-178C. His recent focus is the practical application of neurosymbolic autoformalization to requirements-based verification.

Niranjan Tulpule

Title: Unlocking Safe Agentic Autonomy through Verification

Abstract: As the agentic capabilities of frontier models and frameworks advance, a vast array of tasks across software engineering and knowledge work are being delegated to autonomous systems. Yet, a critical barrier remains: a deficit of trust. Issues of misalignment, probabilistic shortcuts, and containment dominate the current conversation. The proverb “Trust, but verify” has never been more relevant. In this keynote, we will explore the necessity of safely unlocking agentic autonomy. We will make the case for investing in formally provable specifications and deterministic verification techniques across academia and industry which will be paramount to realizing the true, safe impact of Agentic AI.

Bio: Niranjan leads the Developer AI and Core Labs portfolio within Google’s Core Product Area, where he’s revolutionizing how Google’s Software Engineering teams build the products of tomorrow. He oversees the organizations responsible for building AI technologies (models, platforms), developer surfaces, and the telemetry, education, and solutions engineering experiences that empower Google’s developers.

Niranjan is a distinguished engineering leader at Google, with a long tenure and extensive experience across Core, Google Cloud, and Firebase. He has directly influenced key products including Google Desktop Search, Google Chrome, and Gmail, demonstrating profound depth and breadth in Google’s developer ecosystem.

Accepted Papers

Call for Papers

As software systems grow in complexity and autonomy, the gap between stakeholder intent and system implementation widens across the entire development lifecycle. This is a challenge at the heart of modern software engineering: the specification gap. Requirements are often informal and scattered, architectural decisions drift over time, test artifacts only partially capture intent, and legacy codebases frequently lack reliable ground-truth specifications. Re-centering the Software Development Life Cycle (SDLC) around specifications offers a principled path toward alignment, correctness, and maintainability.

SpecOps 2026 advances a vision of Specification-Driven Development Life Cycle (Spec-Driven SDLC), where specifications serve as first-class artifacts spanning requirements, design, implementation, testing, deployment, and evolution. The workshop explores how foundation models (e.g., GPT-4, Claude, Codex, Code Llama) and agentic AI systems can synthesize, refine, validate, and operationalize specifications from heterogeneous sources—including natural language requirements, source code, execution traces, and architectural models—while enabling continuous verification and lifecycle-wide traceability.

Bringing together researchers and practitioners from Software Engineering, Programming Languages, Formal Methods, and Artificial Intelligence, SpecOps 2026 aims to foster dialogue on how AI-powered tools and autonomous agents can transform specifications from static documentation into living, executable, and lifecycle-spanning drivers of modern software and AI system development.

Topics

We welcome contributions on all aspects of specification synthesis, validation, traceability, datasets, including, but not limited to:

Specification Synthesis from Diverse Sources

• Legacy code analysis: Synthesizing formal specifications (temporal logic, contracts, invariants) from undocumented source code
• Automated Formalization: Translating natural language requirements and user stories into structured, unambiguous formal specifications
• Multi-modal synthesis: Combining code, documentation, test suites, execution traces, and architectural diagrams for comprehensive specification extraction
• Specification-grounded code translation: Using synthesized specifications to ensure semantic preservation during code migration and modernization

Downstream Applications

• Formal verification: Using AI-synthesized specifications for model checking, theorem proving, and static analysis
• Testing and validation: Leveraging specifications for test generation, oracle construction, and regression testing
• AI-assisted development: Specifications as prompts and constraints for code generation agents
• Compliance and certification: Automated extraction of safety/security properties for regulatory compliance

Validation, Evaluation and Human Oversight

• Specification validation: Techniques for assessing correctness, completeness, and consistency of AI-generated specifications, LLM-as-a-judge, Constitutional AI
• Interactive refinement: User-guided iterative improvement of synthesized specifications with explainability
• Evaluation metrics: Defining what makes a “good” specification and measuring synthesis quality
• Uncertainty quantification: Confidence estimation and hallucination detection in LLM-generated specifications
• Human Aspects: Role of developer expertise in AI-assisted specification generation, scalability of human-in-the-loop validation approaches.

Traceability and Evolution

• Traceability automation: Mapping synthesized specifications back to source artifacts (commit histories, architectural decisions, design documents, requirements)
• Specification maintenance: Co-evolution of code and specifications, detecting specification drift
• Change impact analysis: Using specifications to predict and assess the impact of code modifications

Datasets and Benchmarks

• Benchmark datasets: Curated collections of code-specification pairs for training and evaluation
• Industrial case studies: Real-world legacy systems and specification synthesis challenges from industry
• Evaluation frameworks: Standardized protocols for comparing specification synthesis approaches
• Data collection and annotation: Methods for creating high-quality training data for specification synthesis models

Submission Details

We invite three types of submissions:

• Full Papers (page limit: 10 pages, including appendix + 2 pages for references) describing original theoretical or empirical research, new techniques, methods for emerging systems, in-depth case studies and industrial experience reports.
• Short Papers (page limit: 4 pages, including appendix + 1 page for references ) that fall into the following categories:
  • Short Research Papers: Preliminary results, Vision papers, Position papers.
  • Tool Demonstration Papers: Descriptions of tools and systems with live demos at the workshop.
  • Dataset Papers: Descriptions of benchmark datasets and evaluation corpora with an associated artifact.
• Extended Abstracts (page limit: 4 pages, including appendix + 1 page for references ) that fall into the same categories as short papers. While the content is the same as short papers, extended abstracts are not subject to Article Processing Charges (APCs; see https://libraries.acm.org/acmopen/article-types).

Submission Guidelines

Submissions must adhere to the ACM SIGPLAN style (acmart format - sigplan subformat, see http://www.sigplan.org/Resources/Author/#acmart-format for detailed instructions) and must be submitted via the SpecOps 2026 author interface of HotCRP ( https://specops26.hotcrp.com). Submission should be in the two-column proceedings format, usually following the LaTeX document class acmart with option sigplan (SIGPLAN/SPLASH-associated) or sigconf (SIGSOFT/ISSTA-associated).

It is recommended to use the review option when submitting a paper; this option enables line numbers for easy reference in reviews. All papers (Full research paper, Short research paper, Tool demonstration paper, Dataset papers) will undergo a double-blind review process. Author(s) name(s) and address(es) must not appear in the body of Full Papers, and self-reference should be avoided and made in the third person.

Proceedings

All accepted Papers will be published by ACM and available via the ACM Digital Library. At least one of the co-authors is expected to present the paper during the workshop.