@inproceedings{wen-etal-2026-formally,
    title = "Formally Specifying the Intended Behavior of the Program: {LLM}-Driven Neuro-Symbolic Program Specification Synthesis",
    author = "Wen, Cheng  and
      Junjie, Hu  and
      Hu, YiKun  and
      Su, Jie  and
      Yu, Bin  and
      Liu, Dugang  and
      Xu, Zhiwu  and
      Sun, Weidi  and
      Qin, Shengchao  and
      Tian, Cong",
    editor = "Durrett, Greg  and
      Jian, Ping",
    booktitle = "Proceedings of the 64th Annual Meeting of the {A}ssociation for {C}omputational {L}inguistics (Volume 3: System Demonstrations)",
    month = jul,
    year = "2026",
    address = "San Diego, California, United States",
    publisher = "Association for Computational Linguistics",
    url = "https://preview.aclanthology.org/ingest-acl/2026.acl-demo.66/",
    pages = "672--682",
    ISBN = "979-8-89176-392-0",
    abstract = "Formal verification can provide strong mathematical guarantees about software correctness, but it typically requires developers to write detailed formal specifications (e.g., contracts and loop invariants), which is costly and error-prone. We introduce AutoSpec+, an LLM-driven neuro-symbolic demonstration system that reframes specification writing as constrained structured synthesis: large language models generate candidate specifications at the granularity of proof-relevant program components, while a symbolic verifier acts as a deterministic critic that checks legality, satisfiability, and proof adequacy, rejecting or repairing candidates in an iterative loop. This design turns unconstrained text generation into constrained structured synthesis, substantially reducing hallucinations and producing proof-ready annotations. We evaluate AutoSpec+ on seven benchmark suites, showing strong effectiveness. We release an open-source, Dockerized system with ensemble LLM backends and inter-modular verification support for reproducible demonstration and deployment"
}