# Presentation: 858516

## Finding Feasible Counter-examples when Model Checking Abstracted Java Programs

- Corina S. Pasareanu, Matthew B. Dwyer (Kansas State University)
- and Willem Visser (NASA Ames Research Center)

*http://www.cis.ksu.edu/santos/bandera*

**Notes:**
This is a joint work with Matt Dwyer, Willem Visser.

## Introduction

**Abstractions in Software Verification:**
**used to reduce the data/control domains of a program**
**described as abstract interpretation**
**over-approximation**
**preserve true results**
**abstract counter-examples may be ****infeasible**** **

## Example of Infeasible Counter-example

**[****1] if (-2 + 3 > 0) **
**    ****then**
**[2]     assert(true);**
**    ****else**
**[3]     assert(false);**

***Signs:***
**n < 0 -> neg**
**  ****0   -> zero**
**n > 0 -> pos**

**[1] if(Signs.gt(Signs.add(NEG,POS),ZERO))**
**    ****then**
**[2]     assert(true);**
**    ****else**
**[3]     assert(false);**

## Problem

**Finding the abstract counter-examples that represent real program ****defects**
**Previous work: **
**after model checking; analyze the counter-example to see if it is feasible**
**pre-image computations (InVest) **
**symbolic execution (SLAM)**
**forward simulation (CMU)**

## Our Solutions

**Choice-bounded State Space Search**
**“****on-the-fly”, during model checking**
**Abstract Counter-example Guided Concrete Simulation**
**Exploit implementations of abstractions for Java programs**
**Effective in practice**

**Notes:**
compare with previous work
 say what are these observations
- experience with defective Java applications

## Abstractions for Java Programs

**Program Abstraction**
**over-approximation**
**using “internal” non-determinism**
**Property Abstraction**
**under-approximation**
**Scheduler Abstraction**
**Java: weak specification of scheduler**
**threads are assigned priorities**
**“****All threads with top priority will eventually run” **

**Notes:**
- Syntactic convention: difference between internal and external non-determinism

## Abstract Interpretation

**abstraction Signs abstracts int**
**  ****TOKENS = { *****neg*****, *****zero*****, *****pos***** };**
**  **
** ****abstraction mapping:**
** **
**        ****n  <  0   -> {*****neg*****};**
**        ****n  ==  0  -> {*****zero*****};**
**        ****n  >  0   -> {*****pos*****};**

**public class Signs {**
**  ****public static final int NEG  = 0; **
**  ****public static final int ZERO = 1; **
**  ****public static final int POS  = 2; **
**  **
**  ****public static int abs(int n) {**
**    ****if (n < 0) return NEG;**
**    ****if (n == 0) return ZERO;**
**    ****if (n > 0) return POS;**
**  ****}**
**  ****public static int add(int a, int b){**
**    ****int r; **
**    ****Verify.beginAtomic()****;**
**     ****if (a==NEG  && b==NEG)  r=NEG;**
**     ****if (a==NEG  && b==ZERO) r=NEG;**
**     ****if (a==ZERO && b==NEG)  r=NEG;**
**     ****if (a==ZERO && b==ZERO) r=ZERO;**
**     ****if (a==ZERO && b==POS)  r=POS;**
**     ****if (a==POS  && b==ZERO) r=POS;**
**     ****if (a==POS  && b==POS)  r=POS;**
**     ****else r=****Verify.choose(2)****;**
**    ****Verify.endAtomic()****; **
**    ****return r; }}**

**Notes:**
- Syntactic difference between internal and external non-determinism

- An abstract program is obtained from the concrete program by replacing the concrete data domains with abstract data domains, and concrete primitive operations with calls to methods that implement abstract operations.
- If the abstract program satisfies the abstract property infer that the concrete program satisfies the concrete property.

## Choose-free state space search

**Theorem [Saidi:SAS’00]**
**   ****Every path in the abstracted program where all assignments are deterministic is a path in the concrete program.**
**Bias the model-checker**
**to look only at paths that do not refer to instructions that introduce non-determinism**
**Model checker modified**
**to detect non-deterministic choice (i.e. calls to ****Verify.choose()****); backtrack from those points**

## Choice-bounded Search

**choose(2)**

**X**

**X**

## Counter-example guided simulation

**Use abstract counter-example to guide simulation of concrete program**
**Why it works:**
**Correspondence between concrete and abstracted program**
**Unique initial concrete state (Java defines default initial values for all data)**

## Example of Abstracted Code

***Java Program:***
**   ****class App{**
**    ****public static void main(...) {**
**[1]  new AThread().start(); **
**     ...**
**[2]  int i=0;**
**[3]  while(i<2) {**
**       ...**
**[4]    assert(!Global.done);**
**[5]    i++;**
**    ****}}}**
**   ****class Athread extends Thread {**
**    ****public void run() { **
**     ...**
**[6]  Global.done=true;**
**    ****}}**

**Choose-free counter-example: 1 - 2 - 6 - 3 - 4**

***Abstracted Program:***** **
**   ****class App{**
**    ****public static void main(...) {**
**[1]  new AThread().start(); **
**     ...**
**[2]  int i=Signs.ZERO;**
**[3]  while(Signs.lt(i,signs.POS)){**
**       ...**
**[4]    assert(!Global.done);**
**[5]    i=Signs.add(i,Signs.POS);**
**    ****}}}**
**   ****class Athread extends Thread {**
**    ****public void run() { **
**     ...**
**[6]  Global.done=true;**
**    ****}}**

**Notes:**
Problem: I is abstracted with Signs, the loop condition is abstracted, infeasible counter-examples because the loop gets executed more than 2 times

## Example of Abstracted Code

**Abstract counter-example: 1 - 2 - 3 - 4 - 5 - 3 - 4 - 5 - 3 - 6 - 4**

***Java Program:***
**   ****class App{**
**    ****public static void main(...) {**
**[1]  new AThread().start(); **
**     ...**
**[2]  int i=0;**
**[3]  while(i<2) {**
**       ...**
**[4]    assert(!Global.done);**
**[5]    i++;**
**    ****}}}**
**   ****class Athread extends Thread {**
**    ****public void run() { **
**     ...**
**[6]  Global.done=true;**
**    ****}}**

***Abstracted Program:***** **
**   ****class App{**
**    ****public static void main(...) {**
**[1]  new AThread().start(); **
**     ...**
**[2]  int i=Signs.ZERO;**
**[3]  while(Signs.lt(i,signs.POS)){**
**       ...**
**[4]    assert(!Global.done);**
**[5]    i=Signs.add(i,Signs.POS);**
**    ****}}}**
**   ****class Athread extends Thread {**
**    ****public void run() { **
**     ...**
**[6]  Global.done=true;**
**    ****}}**

## Hybrid Approach

**     ****Choose-free      **
**Model Check**

** ****Abstraction **

**Program & Property**

**Model Check**

**Abstract Program **
**& Property**

**Property true!**

**  ****Property false!**
**(counter-example)**

**Guided Simulation**

**Abstract **
**counter-example**

**Refine selections**

**Mismatch**

## Implementation

**Java PathFinder (JPF):**
**model checker for Java programs**
**built on top of a custom made Java Virtual Machine**
**checks for deadlock and violations of assertions**
**predicate abstraction**
**Bandera’s data abstraction**

## Experience with Java Programs

***     ******Program          Lines****** ******of  # Threads  Abstraction    Size of default    Size of choose-free***
***                                ******code******	******	******	******      counter-example    counter-example***
**                                                                                                                            **
**Remote Agent****	****55****	****   ****3****	****  Signs****	****            74 steps ****	****            40 steps **
**Experiment                                                                                                            **
**	****	****	****                   ****Even-Odd         128 steps****	****             ---**
**  **
**Pipeline ****	****                 ****103****	****   5****	****  Signs****	****          168 steps****	****            69 steps**
**Readers-Writers****    ****590****	****   5****	****  Signs****	****          176****	**** steps                  76 steps**
**DEOS scheduler****   ****1443****	****   6****	****  Signs****	****          471 steps****	****          312 steps**

**Notes:**
RAX (Remote Agent experiment), is a Java version of a component extracted from an embedded spacecraft-control application. 
Pipeline is a generic framework for implementing multi-threaded staged calculations. 
RWVSN is Doug Lea's generic readers-writers synchronization framework. 
DEOS is the scheduler from a real-time executive for avionics systems that was translated from C++. 

## Ongoing Work

**Add “choose-free search” to Bandera SPIN models**
**Programs with inputs **
**“****external” non-determinism(e.g. DEOS)**
**Driving abstraction selection from infeasible counter-examples**
**Empirical comparisons with other existing approaches**
**CTL model checking**

**Notes:**
Use “cheaper” methods to find counter-examples, before using more expensive methods.

## Conclusions

**Two approaches for ****finding defects**** in abstracted programs**
**Fast: **
**choose-free search is depth-bounded**
**cost of simulation depends on the length of the counter-example**
**Complementary to other techniques**

**Notes:**
Punch line

## Spurious Counter-example Introduced by Property Abstraction

***Java Program:***
***   ******...***
**[1]  x=1;**
**[2]  y=x+1;**
**[3]  ****assert(x<y);**
**       **

***Abstracted Program:***** **
**    ****...**
**   **
**[1]  x=Signs.POS; **
**[2]  y=Signs.add(x,Signs.POS);**
**[3]  ****assert((x==Signs.NEG && y==Signs.ZERO)**
**          ****||(x==Signs.NEG && y==Signs.POS)**
**          ****||(x==Signs.ZERO && y==Signs.POS));**** **
**       **

## Hybrid Approach

**Run abstract model check**
**If counter-example**
**run choice-free search**
**If no counter-example**
**run “stronger” approach**
**Can use different tools for different jobs, e.g., SPIN->JPF->SMV**

## Experience

**Defective Java Applications: Pipeline, Readers-Writers, RAX, DEOS (avionics software)**
**Choose-free model checking: **
**choose-free counter-examples are common**
**fast (since it is a depth bounded search) **
**short counter-examples **
**enables more aggressive abstractions**