L16 - Abstractions and Abstract Reachability Graphs

Back to Program Verification Index | Previous: (y-15) Correctness via Assert Statements | Next: (y-17) Infeasibility Proofs and CEGAR

Mental Model for Abstractions

• The State Space Explosion: Programs have too many states to check individually. Abstraction allows us to group many concrete states into one “abstract” state.
• Predicates as Buckets: We use a finite set of formulas (Predicates) $B$ to categorize states. For example, if $B=\{x>0\}$, we only care if $x$ is positive or not.
  • Finite Approximation: This analogy helps understand how we map an infinite number of concrete states (all possible values of $x$) into a finite set of “buckets” defined by our predicates.
• Abstract Reachability Graph (ARG): A graph where each node is an Abstract Configuration $(\ell ,\varphi )$. It represents “at location $\ell$, the program state satisfies $\varphi$.”
• Safety Proof: If we can build an ARG where no node $({\ell }_{\text{err}},\varphi )$ has a satisfiable $\varphi$, we have proven the program safe.

Abstract Strongest Post ($s{p}_B^{\#}$)

The standard $sp$ can produce complex formulas. The Abstract Strongest Post forces the result to be a conjunction of formulas from our set $B$.

$s{p}_B^{\#}(\psi ,st)=\bigwedge \{\varphi \in B\mid sp(\psi ,st)\subseteq \varphi \}$

• Intuition: We take the real strongest postcondition and “round it up” to the nearest combination of predicates we already know.
• This ensures the number of possible abstract states remains finite.

---

Abstract Reachability Graphs (ARG)

An ARG is a way to systematically explore the abstract state space of a program.

Formal Definition

An ARG is a pair $(AC,T)$ where:

• $AC$: A set of abstract configurations $(\ell ,S)$, where $\ell$ is a program location and $S$ is a set of states (represented by a formula).
• $T$: A set of abstract transitions $((1,S),st,({\ell }^{\prime },S^{\prime }))$.

Construction Algorithm

1. Start at the initial location with the precondition: $({\ell }_{\text{init}},{\varphi }_{\text{pre}})$.
2. Explore: For each outgoing edge in the CFG, compute the new abstract state using $s{p}_B^{\#}$.
3. Worklist: Continue until no new abstract configurations are discovered.

---

Safety in the ARG

An ARG is a Safety Proof if:

• For every location ${\ell }_{\text{err}}$ (an error location), the corresponding formula $S$ in $({\ell }_{\text{err}},S)$ is false.
• This means that within our abstraction $B$, it is impossible to reach the error state.

💡 Intuition: Precision vs. Scalability

• If $B$ is too small (e.g., $B=\varnothing$), the ARG will be small but might say the program is “unsafe” even if it’s actually safe (a False Positive).
• If $B$ is too large, the ARG might be too big for a computer to handle, but it will be more precise.

---

Summary

1. Abstraction simplifies the program by focusing on a few key properties (Predicates).
2. $s{p}_B^{\#}$ keeps the reasoning within the bounds of our chosen predicates.
3. ARG is the graph of all reachable abstract states.
4. A program is Safe if its ARG never reaches an error state with a satisfiable formula.
5. The Guesswork: The main challenge in verification is finding a “good” set $B$ that is precise enough to prove safety but small enough to be efficient.

Self-Check

1. What role does the predicate set $B$ play in abstract interpretation, and why must it be finite?

Answer

$B$ is the finite vocabulary the abstraction is allowed to use. Every abstract state is a conjunction of predicates drawn from $B$ (or their negations), which makes the set of possible abstract states finite. Finiteness is what guarantees the ARG construction terminates, even when the concrete state space is infinite.

2. Define $s{p}_B^{\#}(\psi ,st)$ and explain what “rounding up” means.

Answer

$s{p}_B^{\#}(\psi ,st)$ is the conjunction of all $\varphi \in B$ such that $sp(\psi ,st)\subseteq \varphi$. It takes the concrete strongest postcondition and replaces it with the strongest combination of $B$-predicates that is still implied by it, which is generally weaker than the real $sp$. That weakening is the “rounding up” that keeps results inside the predicate vocabulary.

3. What are the two components of an ARG node, and what does the node mean?

Answer

A node is an abstract configuration $(\ell ,\varphi )$ where $\ell$ is a CFG location and $\varphi$ is a formula (a $B$-state) representing a set of concrete states. The node asserts: “when the program reaches $\ell$, the actual state satisfies $\varphi$”.

4. Under what condition does an ARG constitute a safety proof?

Answer

Every node $({\ell }_{\text{err}},\varphi )$ at an error location must have $\varphi$ equivalent to false. That means in the abstraction, no concrete state can be witnessing an assertion failure, and since the ARG over-approximates real reachability, the program is genuinely safe.

5. Describe the trade-off involved in choosing the predicate set $B$.

Answer

A small $B$ yields a small ARG that may be too coarse to prove safety, producing false alarms (the abstraction says an error state is reachable when concretely it is not). A large $B$ gives more precision but explodes the abstract state space and cost. The “guesswork” is finding a $B$ precise enough to prove the property and small enough to scale.

---

Back to Program Verification Index | Previous: (y-15) Correctness via Assert Statements | Next: (y-17) Infeasibility Proofs and CEGAR | (y) Return to Notes | (y) Return to Home