Saved in:
| Main Authors: | , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2508.14532 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913998561083392 |
|---|---|
| author | Wang, Zhongyi Lin, Tengjie Chen, Mingshuai Yang, Mingqi Li, Haokun Yi, Xiao Qin, Shengchao Yin, Jianwei |
| author_facet | Wang, Zhongyi Lin, Tengjie Chen, Mingshuai Yang, Mingqi Li, Haokun Yi, Xiao Qin, Shengchao Yin, Jianwei |
| contents | Fully automated verification of large-scale software and hardware systems is arguably the holy grail of formal methods. Large language models (LLMs) have recently demonstrated their potential for enhancing the degree of automation in formal verification by, e.g., generating formal specifications as essential to deductive verification, yet exhibit poor scalability due to context-length limitations and, more importantly, the difficulty of inferring complex, interprocedural specifications. This paper outlines Preguss - a modular, fine-grained framework for automating the generation and refinement of formal specifications. Preguss synergizes between static analysis and deductive verification by orchestrating two components: (i) potential runtime error (RTE)-guided construction and prioritization of verification units, and (ii) LLM-aided synthesis of interprocedural specifications at the unit level. We envisage that Preguss paves a compelling path towards the automated verification of large-scale programs. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_14532 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Preguss: It Analyzes, It Specifies, It Verifies Wang, Zhongyi Lin, Tengjie Chen, Mingshuai Yang, Mingqi Li, Haokun Yi, Xiao Qin, Shengchao Yin, Jianwei Software Engineering Logic in Computer Science Fully automated verification of large-scale software and hardware systems is arguably the holy grail of formal methods. Large language models (LLMs) have recently demonstrated their potential for enhancing the degree of automation in formal verification by, e.g., generating formal specifications as essential to deductive verification, yet exhibit poor scalability due to context-length limitations and, more importantly, the difficulty of inferring complex, interprocedural specifications. This paper outlines Preguss - a modular, fine-grained framework for automating the generation and refinement of formal specifications. Preguss synergizes between static analysis and deductive verification by orchestrating two components: (i) potential runtime error (RTE)-guided construction and prioritization of verification units, and (ii) LLM-aided synthesis of interprocedural specifications at the unit level. We envisage that Preguss paves a compelling path towards the automated verification of large-scale programs. |
| title | Preguss: It Analyzes, It Specifies, It Verifies |
| topic | Software Engineering Logic in Computer Science |
| url | https://arxiv.org/abs/2508.14532 |