Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods
We investigate how combinations of Large Language Models (LLMs) and symbolic analyses can be used to synthesise specifications of C programs. The LLM prompts are augmented with outputs from two formal methods tools in the Frama-C ecosystem, Pathcrawler and EVA, to produce C program annotations in the specification language ACSL. We demonstrate how the addition of symbolic analysis to the workflow impacts the quality of annotations: information about input/output examples from Pathcrawler produce more context-aware annotations, while the inclusion of EVA reports yields annotations more attuned to runtime errors. In addition, we show that the method infers rather the programs intent than its behaviour, by generating specifications for buggy programs and observing robustness of the result against bugs.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
The Challenges in Specifying and Explaining Synthesized Implementations of Reactive Systems
In formal synthesis of reactive systems an implementation of a system is automatically constructed from its formal specification. The great advantage of synthesis is that the resulting implementation is correct by constr…
NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis
We introduce NeuroSynt, a neuro-symbolic portfolio solver framework for reactive synthesis. At the core of the solver lies a seamless integration of neural and symbolic approaches to solving the reactive synthesis proble…
Active Perception and Control from PrSTL Specifications
Next-generation intelligent systems must plan and execute complex tasks with imperfect information about their environment. As a result, plans must also include actions to learn about the environment. This is known as ac…
Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models
Reactive synthesis, the problem of automatically constructing a hardware circuit from a logical specification, is a long-standing challenge in formal verification. It is elusive for two reasons: It is algorithmically har…
Symbolic LTLf Synthesis
LTLf synthesis is the process of finding a strategy that satisfies a linear temporal specification over finite traces. An existing solution to this problem relies on a reduction to a DFA game. In this paper, we propose a…