# Presentation: 037084

## Combining Predicate and Numeric Abstraction for Software Model Checking

**Combining Predicate and Numeric Abstraction for Software Model Checking**

- Software Engineering Institute
- Carnegie Mellon University
- Pittsburgh, PA  15213
- Arie Gurfinkel and Sagar Chaki

**Notes:**
Title Slide
Title and Subtitle text blocks should not be moved from their position if at all possible.

## Automated Software Analysis

**Program**

**Automated**
**Analysis**

- Correct

- Incorrect

- Software Model Checking with Predicate Abstraction
- e.g., Microsoft’s SDV

- Abstract Interpretation with Numeric Abstraction
- e.g., ASTREE, Polyspace

## Predicate and Numeric Abstractions

**Predicate Abstraction (PA) (e.g., SDV)**
- Typical property: no lock is acquired twice
- Reduces program verification to propositional reasoning with model checker
- Works well for control-driven programs, and poorly for data-driven programs
**Numeric Abstraction (NA) (e.g, ASTREE)**
- Typical property: no arithmetic overflow
- Reduces program verification to arithmetic reasoning
- Works well for data-driven programs, and poorly for control-driven programs
**How to combine PA and NA to get the best of both?!**

## Outline

**Predicate and Numeric Abstract for Program Analysis**
**Strength and Weakness**
**An “Ideal” Combination**
**PA+NA Combination**
**Abstract Transformers**
**Data Structures**
**Experimental Results**
**Current and Future Work**

## Predicate Abstraction: An Example

**Program**

**p1:i=1  p2:i=2  **
**p3:x1>0  p4:x2<0**

**Pred. Abstraction**

**assume (i=1 || i=2)**
**if (i = 1) **
**  ****x1 := i; **
**else if (i = 2)**
**  ****x2 := -4;**
**if (i = 1)**
**  ****assert (x1 > 0);**
**else if (i = 2)**
**  ****assert (x2 < 0);**

**assume (p1 || p2)**
**if (p1) **
**  ****p3 := ch(p1||p2,false); **
**else if (p2)**
**  ****p4 := true**
**if (p1)**
**  ****assert (p3);**
**else if (p2)**
**  ****assert (p4);**

## Analysis with Predicate Abstraction

**p1:i=1  p2:i=2  **
**p3:x1>0  p4:x2<0**

**Pred. Abstraction**

**assume (p1 || p2)**
**if (p1) **
**  ****p3 := ch(p1||p2,false); **
**else if (p2)**
**  ****p4 := true**
**if (p1)**
**  ****assert (p3);**
**else if (p2)**
**  ****assert (p4);**

**p1 || p2**

**p1**

**p1&&p3**

**!p1&&p2&&p4**

**p1&&p3**
**||**
**!p1&&p2&&p4**

**!p1&&p2**

**p2&&p4**

**p1&&p3**

## Predicate Abstraction Strength/Weaknesses

**Strengths**
**Works well for control-dependent properties**
**Completely automated**
**Predicates can come from any theory that has an automated (semi-)decision procedure **
**Supports any Boolean combination of predicates**
**Compatible with CounterExample Guided Abstraction Refinement**
**Weaknesses**
**Scalability (construction and analysis)**
**Restricted to finite abstract domains**

## Numeric Abstract Interpretation

**Analysis is restricted to a fixed Abstract Domain **
**Abstract Domain is “a restricted (possibly infinite) set of predicates” + efficient operations.**
**Examples of Numeric Abstract Domains**
- Signs	         0 < x,   x = 0,   x > 0
- Intervals	         c1 <= x <= c2,  where c1,c2 are a constants
- Octagons          ± x ± y <= c,  where c is a constant
- Polyhedra         a1x1 + a2x2 +a3x3 + a4 <= 0, where a1,a2,a3,a4 are constants

## AbsDom Interface

**interface** AbsDom(V)
-     A – abstract elements, E – expressions, S -- statements
**α** : E → A		 **γ** : A → E		     **meet** : A x A → A
**isTop** : A → bool	 **isBot** : A → bool	     **join** : A x A → A
**leq** : A x A → bool	 **α****Post** : S → (A → A)         **widen** : A x A → A
- All operations are over approximations,  e.g.,
**γ** (a) || **γ** (b)   => **γ** ( **join** (a, b) )
**γ** (a)  && **γ**** **(b) => **γ** (**meet** (a,b) )

## Example: The Domain of Intervals

- (1, 10) **meet** (2, 12) = (2,10)

- (1, 3) **join** (7, 12) = (1,12)

- (a, b) **meet** (c, d) = (max(a,c), min(b,d))

- (a, b) **join** (c, d) = (min(a,c),max(b,d))

**α****Post** (x := x + 1) ((a, b)) = (a+1, b+1)

- (1, 10) + 1 = (2, 11)

**Operations**

**Examples**

- over-approx

## Analysis with Intervals NA (1)

**assume (i=1 || i=2)**
**if (i = 1) **
**  ****x1 := i; **
**else if (i = 2)**
**  ****x2 := -4;**
**if (i = 1)**
**  ****assert (x1 > 0);**
**else if (i := 2)**
**  ****assert (x2 < 0);**

**1 <= i <= 2**

**i=1**

**i=1 && x1=1**

**i=2**

**i=2 && x2=-4**

**1 <= i <= 2**

**i=1**

**i=2**

## Analysis with Intervals NA (2)

**if (3 <= y1 <= 4) {**
**  ****x1 := y1-2; **
**  ****x2 := y1+2; **
**}**
**else if (3 <= y2 <= 4) {**
**  ****x1 := y2-2; **
**  ****x2 := y2+2; **
**}**
**else return;**
**assert (5 <= x1 + x2 <= 10);**

**3 <= y1 <= 4**

**3 <= y1 <= 4**
**1 <= x1 <= 2**
**5 <= x2 <= 6**

**3 <= y2 <= 4**

**3 <= y2 <= 4**
**1 <= x1 <= 2**
**5 <= x2 <= 6**

**1<=x1<=2**
**5<=x2<=6**

## Strength/Weakness of Numeric Abstraction

**Strength**
**Fully Automated**
**Scalable**
**Supports infinite abstract domains**
**(Supports) Automated Refinement**
**Weakness**
**Limited to a few theories (intervals, octagons, polyhedra)**
**Restricted to conjunctions of terms**
**Looses precision very quickly (join, widen, etc.)**

## “Ideal” combination of PA + NA

**p: A[y1+y2]=3 **
**q: A[x1+x2]=3**

**assume (x1 = x2);**
**if (p) {**
**  ****x1 := y1 – 2 && q := *;**
**  ****x2 := y2 + 2 &&**
**   ****q := ch ((x1=y1-2)&&p,f)**
**} else**
**  ****q := false;**
**if (q) {**
**  ****x1 := x1 + x2;**
**  ****x2 := x2 + y1; **
**}**
**assert (x1 = x2)**

**“****Ideal” combination of PA + NA**

**assume (x1 = x2);**
**if (A[y1+y2] = 3) {**
**  ****x1 := y1 – 2;**
**  ****x2 := y2 + 2;**
**} else**
**  ****A[x1+x2] := 5;**
**if (A[x1+x2] = 3) {**
**  ****x1 := x1 + x2;**
**  ****x2 := x2 + y1; **
**}**
**assert (x1 = x2)**

**Predicates:**** p: A[y1+y2]=3, q: A[x1+x2]=3**

## “Ideal” combination of PA + NA

**p: A[y1+y2]==3 **
**q: A[x1+x2]==3**

**“****Ideal” combination of PA + NA**

**assume (x1 = x2);**
**if (A[y1+y2] = 3) {**
**  ****x1 := y1 – 2;**
**  ****x2 := y2 + 2;**
**} else**
**  ****A[x1+x2] := 5;**
**if (A[x1+x2] = 3) {**
**  ****x1 := x1 + x2;**
**  ****x2 := x2 + y1; **
**}**
**assert (x1 = x2)**

**assume (x1 = x2);**
**if (p) {**
**  ****x1 := y1 – 2 && q := *;**
**  ****x2 := y2 + 2 &&**
**   ****q := ch ((x1=y1-2)&&p,f)**
**} else**
**  ****q := false;**
**if (q) {**
**  ****x1 := x1 + x2;**
**  ****x2 := x2 + y1; **
**}**
**assert (x1 = x2)**

**Predicates:**** p: A[y1+y2]=3, q: A[x1+x2]=3**

## Analyzing with PA + NA

**assume (x1 = x2);**
**if (p) {**
**  ****x1 := y1 – 2 && q := *;**
**  ****x2 := y2 + 2 &&**
**   ****q := ch ((x1+2 = y1)&&p,f)**
**} else**
**  ****q := false;**
**if (q) {**
**  ****x1 := x1 + x2;**
**  ****x2 := x2+y1-2; **
**}**
**assert (x1 = x2)**

**x1=x2**

**p && x1=x2 **

**p && x1=y1-2 **

**p && x1=y1-2 && **
**x2=y2+2 && q **

**!p && !q && x1=x2**

**p && x1=y1-2 && **
**x2=y2+2 && q**
**||**
**!p && !q &&**
**x1=x2 **

**p && x1=y1-2 && **
**x2=y2+2 && q **

**p && x1=y1+y2 && **
**x2=y2+2 && q **

**p && x1=y1+y2 && **
**x2=y2+y1 && q **

**Predicates:**** p: A[y1+y2]=3, q: A[x1+x2]=3**

## Grammar for Our Abstract Transformer

- τ   ::= (e? τN) && τP            |
-                 τ || τ                     |                                     (nondet)
-                 τ ; τ                                                                (sequence)
- e   ::= boolean expression over predicate and numeric terms
- τP ::=   p := ch (e, e)          |
-             τP && τP                                         (parallel)
- τN ::= assignment to numeric terms

## Transformer Examples

**Predicates:**** p****1****:z=&x, p****2****:z=&y, p****3****:y=1**

**Concrete**
**Transformer**

**Abstract**
**Transformer**

- assume (*z > 0)

- (p1&&x>0 || p2&&y>0 || !p1&&!p2 )? skip

- *z = u + 1

- (p1? x := u + 1)     ||
- (p2 ? y := u+1)      ||
- (!p1 && !p2 ? skip)

- y = x && x = (y-1? v : w)

- (p3 ? x := v || !p3 ? x := w) &&
- p3 := ch (x=1,x!=1)

## Overview of Our 4 Data Structures

| Name | Example | Num. Terms |
| --- | --- | --- |
| NEXPoint | (p||q) && (0 <= x <= 5) | Explicit
 |
| NEX | (p&& 0<=x<=3) || (!p && (1<=x<=5)) |  |
| MTBDD | (p&& 0<=x<=3) || (!p && (1<=x<=5)) | Symbolic
 |
| NDD | (p && (x=0 || x=3)) || (!p && (x=1 || x=5)) |  |

## NEXPoint

**(P, N)**

**NEXPoint elements are of the form:**

- BDD over
- predicates

- Element of
- numeric
- abstract domain

**All operations are pairwise**

## Numeric EXplicit (NEX)

**NEX elements are lists of NEXPoint**

**[(P****1****, N****1****),..., (P****k****,N****k****)]**

**Satisfying the partitioning condition**

**P****i**** ****∩**** P****j**** = { }**

**Operations are done using NEXPoint, **
**but respect the partitioning condition**

## The Partitioning Condition

**p**

**!p**

**q**

**!q**

**x>0**

**x>0**

**y>0**

**y>0**

## Multi-Terminal Numeric Decision Diagrams

- b1

- b2

- x>0 && x=y

- 1-edges are black, 0-edges are red
- edges to 0 node are not shown

- p1 && !p2 && (x>0) && (x=y)

- p1: x>0, p2: z<y

- b1: p1, b2: p2

**MTNBDD**

**MTNDD elements are **
**	****Decision Diagrams with Numeric values at the terminals**

## Numeric Decision Diagrams

- (p1&&p2) ||
- (x<0 && y=z)

- (x>=0 && z>0) ||
- (!(x>=0) && y=z)

- p1: x>=0, p2: z>0

- b1:x>=0, b2:z>0, b3:y=z

- b1

- b2

- b3

- 1

- 1-edges are black, 0-edges are red
- edges to 0 node are not shown

- normalize

**NDD elements are**
**	****BDDs over Predicate and Numeric Terms**

## Summary of the Data Structures

|  | Precision | Scalability | PA alone | NA alone | Prop Op | Num Op |
| --- | --- | --- | --- | --- | --- | --- |
| NEXPoint | - | ++ | + | ++ | ++ | ++ |
| NEX | + | - | + | ++ | - | ++ |
| MTNDD | + | - | + | + | + | - |
| NDD | ++ | + | + | - | ++ | -- |

## Experimental Results

**Java Implementation**
**Numeric domains implemented on top of Apron library **
**Synthetic examples used to validate specific conjectures**
**NEX & MTNDD better than NDD when numeric joins are exact**
**Since NDD uses exact unions while others use numeric join**
**NDD better than others when invariants are propositionally complex**
**Since NDD has the most sharing capability**
**Realistic examples used to gauge overall performance**
**Total 11 examples: Zitser buffer overflow (3), OpenSSL (2), metal-casting plant controller (4), Micro-C OS (2)**

## Experimental Results

| Domain | #Exp. | Total | Gamma | Join | alphaPost | Image |
| --- | --- | --- | --- | --- | --- | --- |
| Numeric | 7 | 5.7 | 1.5 | 0.4 | 0.5 | 0.3 |
| Predicate | 9 | 133.0 | 0.1 | 0.1 | 0.5 | 0.1 |
| NEXPoint | 10 | 19.0 | 0.8 | 0.9 | 4.5 | 5.0 |
| NEX | 11 | 25.6 | 0.9 | 2.6 | 4.5 | 6.3 |
| MTNDD | 11 | 35.3 | 0.03 | 0.6 | 2.7 | 20.4 |
| NDD | 11 | 23.7 | 0.06 | 0.4 | 2.0 | 10.2 |

**(all times are in seconds)**

## Related Work

**Abstract Interpretation [CC’92]**
**Our domain ****≈ reduced direct product of Predicate and Numeric domains**
**Jain et al. [CAV’06] **
**Applies numeric invariants to simplify predicate abstraction**
**Weaker than NEXPoint**
**Fischer et al. [FSE’05], Beyer et al. [CAV’07,CAV’06] **
**Predicate abstraction + Abstract Domain**
**Similar to NEXPoint, but with simpler transfer functions**
**Bultan et al. [TOSEM’00]**
**MC of programs with Boolean and numeric variables using Omega library**
**Similar to NEX, but with simpler transfer functions**

## Current and Future Work

**We are working on a more comprehensive benchmark suite**
**Need automated abstraction-refinement for PA + NA**
**In the current implementation, the abstract domain is treated as a black box. We are exploring a tighter integration between predicate and numeric domains**
**smarter numeric transfer functions,**
**smarter DD variable ordering, etc.**

## Slide 30