# Presentation: 535880

## Verification of Java Programs using Symbolic Execution and Loop Invariant Generation

- Corina Pasareanu (Kestrel Technology LLC)
- Willem Visser (RIACS/USRA)
- Automated Software Engineering Group
- NASA Ames

## Outline

- Motivation and Overview
- Examples
- Symbolic Execution and Java PathFinder
- Program Verification and Invariant Generation
- Experiments
- Related Work and Conclusions

## Motivation

- Software errors can be very costly.
- Software verification is recognized as an important and difficult problem.

- More recently ...

## Java PathFinder with Symbolic Execution

- Previous work:
- Java PathFinder (JPF) - explicit-state model checker for Java
- Extended with symbolic execution [TACAS’03]
- Motivation
- Open systems, large input data domains
- Complex data structures
- Applications: test-input generation, error detection
- Shortcoming: cannot *prove* properties of looping programs
- New:
- Invariant generation to deal with loops

## Verification Framework Overview

- Uses symbolic execution
- Requires annotations
- method preconditions
- loop invariants
- Novel technique for invariant generation
- uses invariant strengthening, approximation, and refinement
- handles boolean and numeric constraints, dynamically allocated structures, arrays

## Array Example 1

- //** ****precondition**: a!=null;
**public** **static** **void** set(**int** a[]) {
-   **int** i = 0;
-   **while** (i < a.length) {
-     a[i] = 0;
-     i++;
-   }
-   **assert** a[0] == 0;
- }

***Loop invariants:***
* **0**≤**i*
* **¬(a[0]******** 0 **** 0<i)*

## Array Example 2

- //** ****precondition**: a!=null;
**public** **static** **void** set(**int** a[]) {
-   **int** i = 0;
-   **while** (i < a.length) {
-     a[i] = 0;
-     i++;
-   }
**  ****assert** forall int j: a[j] == 0;
- }

***Loop invariant:***
*¬(a[j] ******** 0 **** a.length ≤ i **** 0 ≤  j < a.length) **** *
*¬(a[j] ******** 0 **** j < i **** 0 ≤  i,j < a.length)*

## Symbolic Execution

- Execute a program on symbolic input values
- For each path, build a path condition
- condition on inputs in order for the execution to follow that path
- check satisfiability of path condition
- Symbolic state
- symbolic values/expressions for variables
- path condition
- program counter
- Various applications
- test case generation
- program verification
- Traditionally: sequential programs with fixed number of integers

## Swap Example

- x = 1, y = 0
- 1 > 0 ? true
- x = 1 + 0 = 1
- y = 1 – 0 = 1
- x = 1 – 1 = 0
- 0 > 1 ? false

**Swap Example**

**int** x, y;
**if**** **(x > y) {
-   x = x + y;
-   y = x – y;
-   x = x – y;
-   **if**** **(x > y)
-     **assert** false;
- }

**Concrete Execution Path:**

**Code that swaps 2 integers:**

## Swap Example

**Swap Example**

- [PC:true] x = X, y = Y

- [PC:true] X > Y ?

- [PC:X>Y] y = X + Y – Y = X

- [PC:X>Y] Y > X ?

**int** x, y;
**if **(x > y) {
-   x = x + y;
-   y = x – y;
-   x = x – y;
-   **if **(x > y)
-     **assert** false;
- }

**Code that swaps 2 integers:**

**Symbolic Execution Tree:**

- [PC:X≤Y] END

- [PC:X>Y] x = X+Y

- false

- true

- [PC:X>YY≤X ] END

- [PC:X>YY>X] END

- false

- true

**Notes:**
Say what PC represents: precondition for the inputs to follow a particular path

## Generalized Symbolic Execution

- Handles
- dynamically allocated data structures, arrays
- preconditions, concurrency
- Uses JPF
- to generate and explore the symbolic execution tree
- Implementation via instrumentation
- programs instrumented to enable JPF to perform symbolic execution
- Omega library used to check satisfiability of numeric path conditions (for linear integer constraints)
- lazy initialization for arrays and structures

**Notes:**
Say we use omega library

## Instrumentation

**void** set (**int** a[]) {
-   **int** i = 0;
-   **while** (i < a.length) {
-     a[i] = 0;
-     i++;
-   }
-   **assert** a[0] == 0;
- }

**void** set() {
-   **IntArrayStruct** a = **new** IntArrayStruct();
-   **Expression** i = **new** IntConstant(0);
-   **while** (i._LT(a.length)) {
-     a._set(i,0);
-     i = i._plus(1);
-   }
-   **assert **a._get(0)._EQ(0);
- }

- Instrumented code

**Notes:**
Say where pc is updated

## Library classes

**Library classes**

**class Expression **{ ...
-   **static PathCondition** pc;
-   **Expression** _plus(**Expression** e) {...}
-   **boolean** _LT(Expression e) {
-      **return** pc._update_LT(**this**,e);
-   } }
**class PathCondition** { ...
-   **Constraints** c;
-   **boolean** _update_LT(**Expression** l,
-                                      **Expression** r) {
-     **boolean** result = Verify.choose_boolean();
-     **if**(result)
-         c.add_constraint_LT(l, r);
-     **else**
-         c.add_constraint_GE(l, r);
-     Verify.ignoreIf(!c.is_satisfiable());
-     **return** result; } }

**class **ArrayCell {
**   ****Expression **elem;
**   ****Expression **idx;
- }
**class** IntArrayStruct { ...
-   **Vector** _v;
-   **Expression** length;
**public** Expression _get(**Expression** idx) {
-   Verify.ignoreIf *!inbounds; //assert inbounds*
-   **ArrayCell** cell = _ArrayCell(idx);
-   **return** cell.elem;
- }
**ArrayCell** _ArrayCell(**Expression** idx) {
-   **for**(**int** i=0; i<_v.size(); i++) {
-     **ArrayCell** cell=(**ArrayCell**)_v.elementAt(i);
-     **if**(cell.idx._EQ(idx))
-       **return** cell;
-     }
-     **ArrayCell** ac = **new** ArrayCell(...);
-     _v.add(ac);
-     return ac;
- } }

**Notes:**
Say where pc is updated

## Proving Properties of Programs

- X = init**;**
**while **(C(X))
-       X = B(X);
**assert** P(X);

*Looping program:*

*Program execution:*

**while ...**

- true

**while ...**

- true

**while ...**

- true

**...**

*May be** ****infinite**** ...*
*How to reason about *
*infinite executions?*

*Has**** ******finite**** execution.*
*Easy to reason about!*
***Problem:**** *
*How do we come up with ****Inv****?*
*Requires great user ingenuity.*

**Notes:**
Inv is a boolean expression that is true each time the loop condition is evaluated

## Iterative Invariant Strengthening

*Model check the program:*

- Start with
**Inv****0**** = ¬(¬C ********¬P)**

- Base case violation: error in the program!

- No errors: done, found loop invariant!

- X = init**;**
**assert Inv(X);**
**X = new symbolic values;**
**assume Inv(X);**
**if** (C(X)) {
-       X = B(X);
-       **assert Inv(X); **
- }** else**
**      ****assert** P(X);

**Notes:**
Inv is a boolean expression that is true each time the loop condition is evaluated

## Iterative Strengthening

**Notes:**
Inv is a boolean expression that is true each time the loop condition is evaluated

## Heuristic for Termination

- At each step **k**, apply heuristic for current candidate **Inv****k**

**Notes:**
Inv is a boolean expression that is true each time the loop condition is evaluated

## Iterative Approximation

- Symbolic execution results in finite universe of constraints** ****U****k**

- New constraints** **from **Inv(B(X))**

- Results in **finite** sequence of **approximate**
- invariants:  **Inv****k****1**, **Inv****k****2** ... **Inv****k****m**

**Notes:**
Inv is a boolean expression that is true each time the loop condition is evaluated

## Invariant Generation Method

- Iterative
- strengthening

- Iterative
- approximation

- If there is an error in the program, the method is guaranteed to terminate
- If the program is correct wrt. the property, the method might not terminate

**Notes:**
Inv is a boolean expression that is true each time the loop condition is evaluated

## General Verification Method

- (2) Check the base case and the inductive step
- if both checks return true: done - property true!
- if inductive step fails: apply iterative approximation; go to (2)
- if base case fails for an exact invariant: done - property false!
- if base case fails for an approximate invariant: apply refinement; go to (2)
- If there is an error in the program, the method is guaranteed to terminate
- If the program is correct with respect to the property, the method might not terminate

**Notes:**
Inv is a boolean expression that is true each time the loop condition is evaluated

## Array Example 1

- //** ****precondition**: a!=null;
**public** **static** **void** set(**int** a[]) {
-   **int** i = 0;
-   **while** (i < a.length) {
-     a[i] = 0;
-     i++;
-   }
-   **assert** a[0] == 0;
- }

## Proof

**public** **static** **void** set() {
-   **Expression** i = **new** IntConstant(0);
-   **IntArrayStruct** a = **new** IntArrayStruct();
-   **assert** Inv;
-   i = **new **SymbolicInt();
-   **Verify.ignoreIf **(!Inv); // assume Inv
-   **if **(i._LT(a.length)) {
-          a._set(i,0);
-          i=i._plus(1);
-          print (PC); // oldPC
-          **if **(!Inv)  {
-              print (PC); // PC
-              **assert** false;
-          }
-   } **else**
-          **assert** a._get(0)._EQ(0);
- }

**Inv****0**** = ¬(i ≥ a.length  ******** a[0] ******** 0)**

**Error**

**oldPC: i > 0  ****** **a[0]  ******** 0**

**PC: i > 0  ****** **a[0]  ******** 0** ****** ****(i + 1) ≥ a.length**

**Iterative approximation:**
**Inv****0****1 ****=Inv****0**** ****** **¬oldPC = ¬(i ≥ a.length  ******** a[0] ******** 0)** ******¬(i > 0  ****** **a[0] ******** 0) = ¬(i > 0  ****** **a[0] ******** 0)**

## Proof + tree

- [PC: I<a.length  a[0]0] i=I

**public** **static** **void** set(int [] a) {
-   **int** i = **0**;
-   **assert** Inv;
-   //i,a = new symbolic values;
-   **assume** Inv;
-   **if **(i < a.length) {
-          a[i]=0;
-          i++;
-          // oldPC
-          **if **(!Inv)  {
-              // PC
-              **assert** false;
-          }
-   } **else**
-          **assert** a[0]==0;
- }

**Proof + tree**

**Error**

**Inv****0**** = ¬(i ≥ a.length  ******** a[0] ******** 0)=**
** ****(i<a.length ******** a[0] ******** 0) ****** **(i<a.length ******** a[0] = 0) ****** **(i ≥ a.length  ******** a[0] = 0)**

## Proof + tree

- [PC: I<a.length  a[0]0] i=I

**public** **static** **void** set(int [] a) {
-   **int** i = **0**;
-   **assert** Inv;
-   //i,a = new symbolic values;
**  ****assume** Inv;
-   **if **(i < a.length) {
-          a[i]=0;
-          i++;
-          // oldPC
-          **if **(!Inv)  {
-              // PC
-              **assert** false;
-          }
-   } **else**
-          **assert** a[0]==0;
- }

**Proof + tree**

**Error**

**Inv****0**** = ¬(i ≥ a.length  ******** a[0] ******** 0)=**
** ****(i<a.length ******** a[0] ******** 0) ****** **(i<a.length ******** a[0] = 0) ****** **(i ≥ a.length  ******** a[0] = 0)**

## Proof + tree

- [PC: I<a.length  a[0]0] i=I

**public** **static** **void** set(int [] a) {
-   **int** i = **0**;
-   **assert** Inv;
-   //i,a = new symbolic values;
-   **assume** Inv;
-   **if **(i < a.length) {
-          a[i]=0;
-          i++;
-          // oldPC
-          **if **(!Inv)  {
-              // PC
-              **assert** false;
-          }
-   } **else**
-          **assert** a[0]==0;
- }

**Proof + tree**

**Error**

**Inv****0**** = ¬(i ≥ a.length  ******** a[0] ******** 0)=**
** ****(i<a.length ******** a[0] ******** 0) ****** **(i<a.length ******** a[0] = 0) ****** **(i ≥ a.length  ******** a[0] = 0)**

## Proof + tree

- [PC: I<a.length  a[0]0] i=I

**public** **static** **void** set(int [] a) {
-   **int** i = **0**;
-   **assert** Inv;
-   //i,a = new symbolic values;
**  ****assume** Inv;
-   **if **(i < a.length) {
-          a[i]=0;
-          i++;
-          // oldPC
-          **if **(!Inv)  {
-              // PC
-              **assert** false;
-          }
-   } **else**
-          **assert** a[0]==0;
- }

**Proof + tree**

**Error**

**Inv****0**** = ¬(i ≥ a.length  ******** a[0] ******** 0)=**
** ****(i<a.length ******** a[0] ******** 0) ****** **(i<a.length ******** a[0] = 0) ****** **(i ≥ a.length  ******** a[0] = 0)**

**Error**

- ...

## Array Example 2

- //** ****precondition**: a!=null;
**public** **static** **void** set(**int** a[]) {
-   **int** i = 0;
-   **while** (i < a.length) {
-     a[i] = 0;
-     i++;
-   }
**     ****assert** forall int j: a[j] == 0;
- }

## Proof

**Inv****0**** = ¬(i ≥ a.length  ******** a[j] ******** 0 ******** 0 ≤ j< a.length)**

**oldPC: a[j]  ******** 0 ******** j < i ******** 0 ≤ i,j < a.length**

**Iterative approximation:**
**Inv****0****1 ****=Inv****0**** ****** **¬oldPC = ¬(i ≥ a.length  ******** a[j] ******** 0 ******** 0 ≤ j< a.length)**
**                                     ******** ****¬(a[j]  ******** 0 ******** j < i ******** 0 ≤ i,j < a.length)**

**PC: a[j]  ******** 0 ******** j<i ******** 0 ≤ i,j <a.length ******** ****(i + 1) ≥ a.length**** **

**public** **static** **void** set(int [] a) {
-   **int** i = **0**;
-   **assert** Inv;
-   //i,a = new symbolic values;
-   //j = new symbolic value;
-   **assume** Inv;
-   **if **(i < a.length) {
-          a[i]=0;
-          i++;
-          // oldPC
-          **if **(!Inv)  {
-              // PC
-              **assert** false;
-          }
-   } **else**
-          **assert** a[j]==0;
- }

## Partition Example

**class** Cell {
**int** val;
- Cell next;
- Cell partition (Cell l,** int** v) {
-   Cell curr = l, prev = null;
-   Cell nextCurr, newl = null;
-   **while **(curr != **null**) {
-     nextCurr = curr.next;
**    ****if** (curr.val > v) {
**      ****if** (prev != **null**)
-         prev.next = nextCurr;
-      ** ****if** (curr == l)
-         l = nextCurr;
-       curr.next = newl;
-       **assert** curr != prev;
-       newl = curr;
-     }
-     **else**
-       prev = curr;
-     curr = nextCurr;
-   }
**  ****return** newl; }}

***Loop invariant: ***
*¬(curr=prev ****** curr≠null ****** curr.elem>v) *****
*¬(curr≠* *prev ****** prev≠* *null ****** curr ≠* *null ****** *
*    **prev.elem>v ****** curr.elem>v  ****** prev≠curr.next)*

## Pathological Example

**Pathological Example**

**void** m (**int** n) {
-   **int** x = 0;
-   **int **y = 0;
-  ** ****while** (x <n) {/* loop 1 */
-     x++;
-     y++;
-   }
-   /* hint: x == y */
-   **while** (x!=0) {/* loop 2 */
-     x--;
-     y--;
-   }
-   **assert** y==0;
- }

- First, attempt computation of invariant for loop 2
- Iterative invariant generation does not terminate
- Constraint x=y is important, but not discovered
- Using x=y as a hint we get two invariants:
-   *Loop 2:*
* ****¬(y ************ 0 ************ x=0) ************ ¬(y ≤ 0 ************ x>0) ************ ¬(y>0 ************ x ************y) ***
***  ****Loop 1: *
***¬(x ************ y ************ x ≥ n) ************ ¬(x<0) ************ ¬(x≥0 ************ x<n ************ x ************y)***

## Related Work

- Invariant generation:
- INVEST (Verimag), STEP (Stanford)
- Graf & Saidi (CAV 1996), Havelund & Shankar (FME 1996), Tiwari et al. (TACAS 2001), Wegbreit (CACM 1974)
- ... (a lot of work)
- Iterative forward/backward computations
- Domain specific; focus on numeric invariants
- Heuristics for termination, e.g. using auxiliary invariants
- Abstract interpretation
- Cousot & Cousot (CAV 2002), Cousot & Halbwachs (POPL 1978)
- Widening operator to compute fixpoints systematically
- Flanagan & Qadeer (POPL 2002)
- Loop invariant generation for Java programs
- Uses predicate abstraction
- Predicates need to be provided by the user
- Extended Static Checker (ESC)
- Uses theorem proving to check partial correctness specifications of Java programs
- Rely heavily on user provided specifications, such as loop invariants

**Notes:**
Say we use omega library

## Conclusion and Future Work

- Framework for verification of light-weight specifications of Java programs: new use of JPF
- Iterative technique for discovering (some) loop invariants automatically
- Uses invariant strengthening,  approximation, and refinement
- Handles different types of constraints
- Allows checking universally quantified formulas
- ... Very preliminary work
- Future work:
- Instead of dropping newly generated constraints, replace them with an appropriate boolean combination of exiting constraints from Uk
- Similar to predicate abstraction
- Use more powerful abstraction techniques in conjunction with our framework
- Use heuristics/dynamic methods to discover useful constraints/hints (e.g. Daikon)
- Study relationship to widening and predicate abstraction
- Extend to multithreading and richer properties
- ...

**Notes:**
Say we use omega library