A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs

This paper introduces Preguss, a modular framework that combines static analysis with LLM-aided synthesis to automatically generate and refine interprocedural specifications, enabling highly automated verification of large-scale programs (over 1,000 lines of code) while significantly reducing human effort.

The Gist

Imagine you are the chief inspector for a massive, 1,000-story skyscraper (a large computer program). Your job is to ensure the building is safe: no floors will collapse, no elevators will fall, and no pipes will burst (these are "Runtime Errors").

Traditionally, you have two tools:

1. The Metal Detector (Static Analyzer): It scans the whole building and beeps loudly whenever it thinks it sees a problem. But it's very noisy. It beeps at a harmless coat rack thinking it's a bomb. It beeps at a shadow thinking it's a hole. It gives you thousands of "false alarms."
2. The Architect (The Human Expert): To prove the building is safe, you need blueprints (formal specifications) that explain exactly how every room works. But writing these blueprints for a 1,000-story building by hand takes years and costs a fortune.

The Problem:
Recently, we tried using a super-smart AI (a Large Language Model or LLM) to write these blueprints. But the AI has a short attention span. If you show it the whole 1,000-story building at once, it gets confused and gives up. Also, it doesn't know which blueprints are actually needed to stop the specific alarms the Metal Detector is making. It might write a blueprint for the roof when the alarm is actually about the basement plumbing.

The Solution: Preguss (The Smart Foreman)
The paper introduces Preguss, a new system that acts like a brilliant, organized foreman. It uses a strategy called "Divide and Conquer" to fix the problem.

Here is how Preguss works, using a simple analogy:

1. The "Divide" Phase: Sorting the Alarms

Instead of looking at the whole building at once, Preguss looks at the Metal Detector's list of beeps.

• The Insight: It realizes that most beeps are just noise. It picks one specific beep (e.g., "Potential pipe burst in Room 402") and asks: "What is the absolute minimum set of rules needed to prove this specific room is safe?"
• The Action: It breaks the massive building down into tiny, manageable "inspection units." It creates a to-do list, prioritizing the most critical rooms first. It doesn't try to read the whole building; it just focuses on the specific pipe and the room it's in.

2. The "Conquer" Phase: The AI's Targeted Mission

Now, Preguss sends the AI (the LLM) a very specific, small mission.

• The Prompt: Instead of saying, "Write blueprints for the whole building," it says: "Here is the alarm about the pipe in Room 402. Here is the code for Room 402 and the room directly below it. Write a rule that proves the pipe won't burst."
• The Magic: Because the AI only has to look at a small slice of the building, it doesn't get overwhelmed. It writes a perfect, tiny rule (a "precondition") that says, "As long as the water pressure is below 50 PSI, this pipe is safe."

3. The Feedback Loop: The "Correction" Mechanism

Sometimes, the AI writes a rule that is technically correct but too strict (e.g., "The water pressure must be exactly 0 PSI"). This would cause a new false alarm because real water pressure isn't zero.

• The Fix: Preguss acts like a strict editor. It runs the AI's rule through a "logic checker." If the checker says, "This rule is too strict and will break the building," Preguss sends the rule back to the AI with a note: "You made this too strict. Try again, but be more flexible."
• The AI tries again, gets it right, and the rule is added to the official blueprints.

4. The Result: A Safe Building

By repeating this process for every single alarm, Preguss builds a complete set of safety rules.

• The Win: It turns a task that used to take humans years into a task that takes hours.
• The Efficiency: In the paper's tests, Preguss reduced the human work required by 80% to 89%.
• The Discovery: It didn't just fix false alarms; it actually found 6 real, hidden bugs in a real spacecraft control system that humans had missed!

Summary Analogy

Think of Preguss as a Sherlock Holmes for code.

• Old Way: You hire a detective to read the entire encyclopedia of the city to find one missing sock. They get tired and give up.
• Preguss Way: You tell the detective, "The sock was last seen near the bakery. Go look only at the bakery and the street next to it." The detective finds the sock instantly. If they find a clue that doesn't make sense, they ask for a second opinion, refine the clue, and move on.

Why this matters:
This paper proves that we can finally automate the safety checks for huge, complex software systems (like those in cars, planes, and satellites) without needing a team of 50 experts to spend years writing blueprints. It combines the "noise detection" of traditional tools with the "reasoning power" of modern AI, but with a smart strategy to keep the AI focused and effective.

Technical Summary

Here is a detailed technical summary of the paper "A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs."

1. Problem Statement

The paper addresses the challenge of automatically verifying Runtime Error (RTE) freeness (e.g., division by zero, buffer overflows, null pointer dereferences) in large-scale C programs (over 1,000 lines of code).

• The Bottleneck: While deductive verifiers (like Frama-C/Wp) can prove RTE-freeness, they require precise formal specifications (preconditions, postconditions, loop invariants). Manually writing these for large systems is prohibitively expensive.
• LLM Limitations: Recent attempts to use Large Language Models (LLMs) for specification synthesis fail at scale due to:
  1. Context Window Limits: LLMs cannot process entire large programs as a single context.
  2. Interprocedural Complexity: LLMs struggle to synthesize the diverse set of specifications (contracts, invariants) needed across complex call hierarchies. They often generate "ineffective" postconditions or "over-constrained" preconditions that induce false alarms.
  3. Lack of Guidance: Existing methods do not effectively leverage the specific error locations identified by static analyzers.

2. Methodology: The Preguss Framework

The authors propose Preguss, a modular, fine-grained framework that synergizes Static Analysis (Abstract Interpretation) and Deductive Verification using a Divide-and-Conquer strategy.

Phase 1: Divide (Potential RTE-Guided Construction & Prioritization)

Instead of analyzing the whole program at once, Preguss decomposes the verification task into manageable Verification Units (V-Units).

• Static Analysis: Uses tools like Frama-C/Eva or Frama-C/Rte to generate RTE assertions (guard assertions) pointing to potential undefined behaviors.
• Call Graph Analysis: Constructs a call graph to identify dependencies between functions.
• V-Unit Creation: For each RTE assertion, a V-Unit is created containing:
  • The Guard Assertion (the target to prove).
  • A Minimally Constrained Program Context: The host function and its immediate callees (a two-layer slice). This avoids feeding the entire codebase to the LLM.
• Prioritization: V-Units are ordered in a queue based on a bottom-up verification principle. Functions higher in the call hierarchy (ancestors) are verified after their callees, ensuring that callee contracts are available when verifying the caller.

Phase 2: Conquer (Fine-Grained Interprocedural Specification Synthesis)

Preguss iteratively processes the V-Unit queue using an LLM and a deductive verifier.

• Iterative Refinement: For a given V-Unit, if the verifier cannot prove the guard assertion, it provides feedback (proof obligations).
• Targeted Generation:
  • Host Function: The LLM generates preconditions and loop invariants for the function containing the error, using only the local context to avoid over-constraining.
  • Callee Functions: The LLM generates postconditions for the called functions. Crucially, it is prohibited from generating preconditions for callees to prevent false alarms caused by over-constrained assumptions.
• Feedback-Driven Correction: The verifier checks the generated specifications. If they are syntactically illegal or semantically unsatisfiable (e.g., causing false negatives), the LLM is prompted to correct them.
• Termination: If an assertion cannot be proven, it is marked as a Hypothesis (requiring manual review), and the system proceeds to the next unit, assuming the hypothesis holds.

3. Key Contributions

1. Conceptual Framework: Formalizes Potential RTE-Guided Specification Synthesis, using static analysis alarms as specific targets to guide LLMs, rather than asking them to guess general properties.
2. Preguss System: The first automated method capable of proving RTE-freeness for real-world programs with >1,000 LoC with marginal human effort. It uniquely handles interprocedural specifications by separating host and callee generation strategies.
3. Dataset: Created an open-source dataset of real-world C programs annotated with specifications generated by Preguss and verified by experts.
4. Soundness & Termination: Proves that the framework is sound (if hypotheses are valid, the program is RTE-free) and guaranteed to terminate.

4. Experimental Results

The authors evaluated Preguss on benchmarks (Frama-C-Problems) and four real-world projects: Contiki (544 LoC), X509-parser (1,199 LoC), SAMCODE (1,280 LoC, spacecraft control), and Atomthreads (1,451 LoC).

• Performance vs. Baselines:
  • On the Frama-C-Problems benchmark, Preguss achieved a 79.7% success rate in verifying RTE-freeness, significantly outperforming state-of-the-art LLM baselines (AutoSpec: 32.7%, AutoSpecRte: 41.8%).
  • Baselines often failed to terminate or produced ineffective specifications for large/complex code.
• Scalability: Preguss successfully verified large-scale programs where baselines failed completely.
• Human Effort Reduction:
  • Reduced human verification effort by 80.6% to 88.9% (measured by the number of specifications requiring manual intervention).
  • For the SAMCODE spacecraft system, Preguss automatically verified 87.9% of units and successfully identified 6 genuine RTEs (uninitialized variable accesses) hidden in the code, which were confirmed by developers.
• Cost: While LLM inference costs were higher than baselines (due to iterative refinement), the total time and cost were negligible compared to the months/years of manual effort typically required for such verification.

5. Significance

• Bridging the Gap: Preguss bridges the gap between the scalability of static analysis (which finds errors but has high false positives) and the precision of deductive verification (which requires manual specs).
• Practical Impact: It demonstrates that fully automated verification of industrial-scale software is feasible. The ability to identify real bugs (not just false positives) in a spacecraft control system highlights its utility beyond just "proving" code.
• Methodological Shift: The paper establishes a new paradigm where static analysis guides LLMs (via specific assertions and proof obligations) rather than LLMs attempting to reason about the entire codebase holistically. This "divide-and-conquer" approach effectively mitigates the context window limitations of current LLMs.

In summary, Preguss represents a significant step forward in formal methods, making the verification of large-scale, safety-critical software more automated, scalable, and practical.