L18 - Trace Abstraction and Floyd-Hoare Automata

Back to Program Verification Index | Previous: (y-17) Infeasibility Proofs and CEGAR | Next: (y-19) Constraint-Based Invariant Synthesis

Mental Model for Trace Abstraction

• Code as Language: We can view a program as a Formal Language over an alphabet of statements (e.g., $x:=0$, $x<y$).
• Trace: A “word” in this language is a path through the program (a trace).
• Verification via Automata: Proving safety means showing that every “word” that leads to an error is infeasible (no execution can follow it).
• Trace Abstraction: We build an automaton that “covers” (accepts) many infeasible traces. If we can cover all possible error paths, we have a safety proof.

Programs as Automata

• Alphabet ($\Sigma$): The set of all primitive statements (assignments, assume, assert) in the program. Each edge in the CFG is labeled with an element from $\Sigma$.
• Automaton ($A_P$): The Control-Flow Graph itself is a finite automaton where locations are states and transitions are edges.
• Error Traces: The set of all “words” (traces) accepted by $A_P$ (those starting from ${\ell }_{\text{init}}$ and ending in an error location ${\ell }_{\text{err}}$).

---

Floyd-Hoare Automata

A Floyd-Hoare Automaton (FHA) is a way to prove that many traces are infeasible at once.

Definition

An automaton $A$ is a Floyd-Hoare automaton if there exists a Floyd-Hoare Annotation $\beta$ mapping each state $q\in Q$ to a formula $\varphi$ such that:

1. Inductivity: For every transition $(q,st,q^{\prime })$, the Hoare triple $\{\beta (q)\}st\{\beta (q^{\prime })\}$ is valid.
2. Initial: For initial states $q_0$, $\beta (q_0)=\text{true}$.
3. Safety: For accepting (error) states $q_{err}$, $\beta (q_{err})=\text{false}$.

The Core Theorem

• If a trace is accepted by a Floyd-Hoare automaton, it is infeasible.
• This is because the annotation $\beta$ along the accepting path forms an Infeasibility Proof.

---

The Trace Abstraction Algorithm

1. Step 1: Pick an Error Trace. Find a path $\pi$ in the program’s CFG that leads to an error.
2. Step 2: Prove Infeasibility. Show that $\pi$ is infeasible.
3. Step 3: Construct a Floyd-Hoare Automaton.
   • Build an automaton $A_i$ that accepts $\pi$.
   • Generalize $A_i$ (add extra transitions and states) to accept as many other infeasible traces as possible.
4. Step 4: Subtract and Repeat.
   • Consider only the remaining error traces: $L(A_P)\setminus L(A_1\cup \cdots \cup A_i)$.
   • If there are no traces left, the Program is Safe.
   • Otherwise, go back to Step 1.

---

💡 Intuition: The Blanket Analogy

Imagine a field (the set of all possible error traces $L(A_P)$).

• Some traces are feasible (real bugs).
• Some are infeasible (safe but hard to analyze).
• Trace Abstraction is like placing “blankets” (Floyd-Hoare Automata) over the field. Each blanket covers a set of infeasible traces.
• The Goal: If you can cover the entire set of potential error traces ($L(A_P)$) with these “blankets” without any of them covering a real bug, you have proven the program safe.

---

Summary

1. Trace Abstraction treats verification as an automata-theoretic problem.
2. Alphabet: The program’s statements.
3. Floyd-Hoare Automata: Automata that only accept infeasible traces.
4. Proof of Safety: A program is safe if all its error traces can be covered by a finite set of Floyd-Hoare automata.
5. Ultimate Automizer: This is the core algorithm used in one of the most successful modern verifiers.

Self-Check

1. What is the alphabet over which program traces are words in trace abstraction?

Answer

The alphabet $\Sigma$ is the set of primitive program statements: assignments, havocs, and assumes (including the assume B / assume !B produced by branches and asserts). Each CFG edge is labelled with a letter of $\Sigma$, and a trace is a sequence of such letters.

2. State the three conditions that make an annotation $\beta$ a Floyd-Hoare annotation for an automaton.

Answer

Initial: $\beta (q_0)=\text{true}$ for every initial state. Inductivity: for every transition $(q,st,q^{\prime })$, the Hoare triple $\{\beta (q)\}st\{\beta (q^{\prime })\}$ is valid. Safety: $\beta (q_{\text{err}})=\text{false}$ for every accepting state. Any trace accepted by such an automaton is infeasible.

3. Why does the Floyd-Hoare automaton accepting a trace prove that trace infeasible?

Answer

Along an accepting path the annotation forms a sequence $\beta (q_0),\beta (q_1),\dots ,\beta (q_{\text{err}})$. The conditions force $\beta (q_0)=\text{true}$, every consecutive pair to be Hoare-valid, and $\beta (q_{\text{err}})=\text{false}$. That is exactly an infeasibility proof for the trace.

4. Outline the trace-abstraction algorithm.

Answer

Pick an error trace $\pi$ in the program automaton $A_P$, prove it infeasible, and build a Floyd-Hoare automaton $A_i$ that accepts $\pi$ and generalizes to other infeasible traces. Then look at the remaining error traces, $L(A_P)\setminus L(A_1\cup \cdots \cup A_i)$. If the difference is empty, the program is safe; otherwise pick another remaining trace and repeat.

5. Use the blanket analogy to describe what “safety” means in trace abstraction.

Answer

The program automaton’s error language is a field; each Floyd-Hoare automaton is a blanket covering a set of infeasible traces. Safety means the union of all blankets covers the entire error language without any blanket covering a feasible (real bug) trace, so every potential error path is certified infeasible.

---

Back to Program Verification Index | Previous: (y-17) Infeasibility Proofs and CEGAR | Next: (y-19) Constraint-Based Invariant Synthesis | (y) Return to Notes | (y) Return to Home