# Presentation: 947364

## Abstraction and Modular Reasoning for the Verification of Software

***Corina Pasareanu,***
***October, 2001****** ***

- _Thesis Committee:_
- Matthew Dwyer, Major Advisor
- David Schmidt
- Michael Huth
- George Strecker
- Kenneth Kemp, Outside Chairperson

**Notes:**
This afternoon I will describe some of our recent work that is aimed at abstracting Java programs for verification.  This work has been done in the context of the Bandera project at Kansas State University.

## Finite-state Verification

**Notes:**
Within the bandera project, we are interested in applying fsv technologies to complex software systems.

In fsv, for ex in mc, we describe a program’s comput.behavior as a fs trans.system, we specify a program’s property in some complementary formalism, like temp. logic, and we check exhaustively that the prop. Holds at each state of the system.

The result of verif can be either: ok the property holds on the sys., or no, the prop.does not hold on the sys.and here is a counterex.

## Finite-state Verification of Software 

**Techniques for checking correctness of concurrent programs:**
**Formal verification**
**That a program satisfies a complete specification**
**Dynamic methods/testing**
**That examine the outcome of executions of the program**
**That check assertions during executions**
**Finite state verification (FSV)**
**Automated (like testing)**
**Guarantees satisfaction of properties (like formal verification)**
**Useful for debugging (counter-examples)**
**FSV is a potential very useful technique for insuring high-quality software**

**Notes:**
Instead of analyzing the counter-ex for feasibility, we re-run Java Path Finder to do a customized search for feasible counter-examples on the fly, during verification of the abstracted program.
This resulted in a ...... 

## Finite State Verification of Software

*Creation of tractable models*
*... **software has large/infinite state space*
*Modular reasoning about software components*
*... **using tools that reason about complete systems*

*Abstract interpretation *
*... **to reduce the data domains of a program *
*Program completion*
*... **with code for missing components*
*... **use environment assumptions, assume-guarantee paradigm*

**Notes:**
DEOS Transition

In the next several slides, I will show how our abs tool work on a realistic case study. This will also illustrate several of the challenges in abstracting complex softw systems and our approach to addressing these challenges.

## Goals of our work ...

- Develop multiple forms of tool support for ...

*... **abstraction and program completion*
*... **applicable to program source code*
*... **largely automated, usable by non-experts*

- We evaluate the effectiveness of this tool support through...

*... **implementation *
*... **application to real Java and Ada programs*

- We concentrate on building ...

*... **finite-state models, not finite-state tools *

**Notes:**
DEOS Transition

In the next several slides, I will show how our abs tool work on a realistic case study. This will also illustrate several of the challenges in abstracting complex softw systems and our approach to addressing these challenges.

## General Methodology

**Model Checking **
**<********>**

**Counter-example **
**Analysis**

**Data **
**Abstraction**

**Program **
**Completion **

**Abstracted Completed Program **

**Refine Selection**

**Model of Program**** **

**Property **
**False!**

**Translator**

**Partial Program, Property ********Assumption******

## Contributions 

**Integration of existing technologies into a coherent methodology that enables FSV of software systems**
**Development of new technologies:**
**Use of theorem proving to automatically derive abstractions of data types**
**Instrumentation of source code to enable assume-guarantee reasoning about partial programs**
**Two techniques for analysis of abstract counter-examples**
**Formalization and implementation of these technologies**
**Evaluation of technologies on case studies (Java, Ada)**

**Notes:**
Assumptions: local and global

## Context

**The ****Bandera**** toolset (KSU)**
**Collection of program analysis and transformation components**
**Allows users to analyze properties of Java programs**
**Tailor analysis to property to minimize analysis time**
**The Ada translation toolset**
**Java PathFinder ****(NASA Ames)**
**Model checker for Java programs**
**Built on top of a custom made Java Virtual Machine**
**Checks for deadlock and violations of assertions**

**Notes:**
Instead of analyzing the counter-ex for feasibility, we re-run Java Path Finder to do a customized search for feasible counter-examples on the fly, during verification of the abstracted program.
This resulted in a ...... 

## Related Projects 

**The Microsoft Research SLAM project**
**G. Holzmann’s Fever Tool (Bell Labs)**
**Stoller’s stateless checker for Java programs**
**Godefroid’s Verisoft (Bell Labs)**
**David Dill’s Hardware Verification Group**
**Eran Yahav’ s Java checking tool**

**Notes:**
Instead of analyzing the counter-ex for feasibility, we re-run Java Path Finder to do a customized search for feasible counter-examples on the fly, during verification of the abstracted program.
This resulted in a ...... 

## Outline of the Talk

**Introduction**
**Data Abstraction (FSE’98, ICSE’01)**
**Program Completion**
**Abstract Counter-example Analysis**
**Formal Justification**
**Case Studies: Java and Ada Programs**
**Conclusions, Limitations and Future Work**

**Notes:**
Instead of analyzing the counter-ex for feasibility, we re-run Java Path Finder to do a customized search for feasible counter-examples on the fly, during verification of the abstracted program.
This resulted in a ...... 

## Finite-state Verification

- Effective for analyzing properties of hardware systems

- Limited success due to the
- enormous state spaces
- associated with most software systems

- Recent years have seen many efforts to apply those techniques to software

- Widespread success andadoption in industry

## Abstraction: the key to scaling up

**Notes:**
Of course, most people recognize that abstraction is the key to scaling fsv tech. To reasoning about realistic programs.

Abstraction involves creation of a new sys with fewer states, were each state in the abs.sys. Is like a “symbolic” state that actually represents multiple states. A symbolic state may even repres.an infinite number of state.

When building abstractions, we want them to be safe. Safety allows us to infer that if a property is true for the abs system then the prop. Is true for the orig system.
However, because of over-approx., the ability to disprove properties is in general sacrificed.

## Data Type Abstraction

- int x = 0;
- if (x == 0)
-   x = x + 1;

**Data domains**

**Code**

- Collapses data domains via abstract interpretation:

**Notes:**
The technique can be illustrated on this fragment of code; assume we would like to keep only enough info about x to allow the conditional test to be decided. So we only need to know if x is zero or not

for this we could use the signs abstraction that maps integers onto a set of 3 symbolic values:neg,zero,pos

we transform the code so that to operate on the abs domain and it looks like this; here the concrete type int was replaced by abs type signs, concrete constants 0 and 1 were replaced with abs ct 0 and pos; and primitive ops on ints were replaced with calls to some methods that implement the abs.ops.that manipulate abstract values. Ex : equality operator was replaced with a call to method signs.eq and + was replace by  signs.add .

So, how do we apply this abstraction technique to the DEOS example ?
We have to decide which variables to abstract, what abstrations to use and then we have to effectively transform the system to encode the abstractions.

## Our hypothesis (?) 

**Abstraction of data domains is necessary**
**Automated support for **
**Defining**** abstract domains (and operators)**
**Selecting**** abstractions for program components**
**Generating**** abstract program models**
**Interpreting**** abstract counter-examples**
**will make it possible to**
**Scale property verification to realistic systems**

**Notes:**
The DEOS experience makes it clear that abstraction is necessary for model checking of realistic Java programs.  Furthermore,this experience also illustrates the need for several different forms of tool support to achieve abstraction of large programs

What is automated, what is not?

Link to next slide ...
Not java specific, in fact ada....
Now that you’ve seen the basic steps in abstracting a program in  Bandera  I’ll give an overview of  the abstraction components starting with the user’s interface ...

## Abstraction in Bandera

- Abstraction
- Library

- Signs

- Signs

- Signs

- int

- bool

- ....

- Point

- Buffer

**Notes:**
When the abstraction component of Bandera is invoked for some program, a hierarchical table is displayed, that lists all the variables in the program along with their types. The user selects abstractions from a  library for variables that are deemed particularly relevant to the property to be checked. The selection of variables is guided by the Pd info.  

<click> So for example, assume we select Signs for x.  Once this initial selection is made, Bandera uses a type inference phase to attach abstract types to the remaining variables.  

<click>Then the abstraction code generator transforms the program into an abstracted program that operates with abstract types, as I showed on DEOS.
So one remaining issue is where do the abstractions in this library come from?
The library is populated by an expert user who defines abstractions using a special purpose language that we’ve designed called BASL.  For base types, the user only needs to specify the abstract domain and the abstraction  function, and the PVS theorem prover is used to infer the definitions of the abstract operations.  The abstractions are then compiled to a Java representation and held in the library, for reuse. 

## Definition of Abstractions in BASL

- abstraction Signs abstracts int
- begin
-   TOKENS = { NEG, ZERO, POS };
-   abstract(n)
-     begin
-         n  <  0   -> {NEG};
-         n  ==  0  -> {ZERO};
-         n  >  0   -> {POS};
-     end

-  operator + add
-   begin
-    (NEG , NEG)  -> {NEG}  ;
-    (NEG , ZERO) -> {NEG}  ;
-    (ZERO, NEG)  -> {NEG}  ;
-    (ZERO, ZERO) -> {ZERO} ;
-    (ZERO, POS)  -> {POS}  ;
-    (POS , ZERO) -> {POS}  ;
-    (POS , POS)  -> {POS}  ;
-    (_,_) -> {NEG,ZERO,POS};
-    /* case (POS,NEG),(NEG,POS) */
-   end

**Notes:**
In BASL, we can define AI’s. an AI is a collection of 3 components : a domain of abs.values, an abstract function and a collection of abstract op., one for each primitive operation in the program.
-For example, this is the BASL representation of the signs AI, where the abstract domain is the powerset of the set of tokens.
-The abstract ops.are automatically generated using the PVS theorem prover, for example this is the abstract version of +.
-Note that abstract operations can return more than one token.This is because by abstraction, we loose info about abs.values : you will see on the next slide, that imprecision is MODELED as a non-det. choice over the values in the set. 
-So now, how do we use the theorem prover. For ex, this is how we generate the def of abs.op + applied to 2 NEG values. We start  whith set {NEG, ZERO, POS} which  is safe because it covers all the possible results of adding 2 negative numbers.
-We try to eliminate from the set the tokens that we can prove are not possible. We submit to PVS 3 implications : one for each token in the def. Here predicate NEG? ...POS? and ZERO? are defined similarly.
-So we ask PVS : is it true that  by adding 2 neg numbers we can not get a pos. number, and PVS answers yes, so we eliminate POS from the definition,....
-> same technique for all the cases!  

## Compiling BASL Definitions

**abstraction Signs abstracts int**
**begin**
**  ****TOKENS = { NEG, ZERO, POS };**
**  ****abstract(n)**
**    ****begin**
**        ****n  <  0   -> {NEG};**
**        ****n  ==  0  -> {ZERO};**
**        ****n  >  0   -> {POS};**
**    ****end**
** ****operator + add**
**  ****begin**
**   ****(NEG , NEG)  -> {NEG}  ;**
**   ****(NEG , ZERO) -> {NEG}  ;**
**   ****(ZERO, NEG)  -> {NEG}  ;**
**   ****(ZERO, ZERO) -> {ZERO} ;**
**   ****(ZERO, POS)  -> {POS}  ;**
**   ****(POS , ZERO) -> {POS}  ;**
**   ****(POS , POS)  -> {POS}  ;**
**   ****(_,_)-> {NEG, ZERO, POS};**
**   ****/* case (POS,NEG), (NEG,POS) */**
**  ****end**

**public class Signs {**
**  ****public static final int NEG  = 0; // mask 1**
**  ****public static final int ZERO = 1; // mask 2**
**  ****public static final int POS  = 2; // mask 4**
**  **
**  ****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 arg1, int arg2) {**
**    ****if (arg1==NEG  && arg2==NEG)  return NEG;**
**    ****if (arg1==NEG  && arg2==ZERO) return NEG;**
**    ****if (arg1==ZERO && arg2==NEG)  return NEG;**
**    ****if (arg1==ZERO && arg2==ZERO) return ZERO;**
**    ****if (arg1==ZERO && arg2==POS)  return POS;**
**    ****if (arg1==POS  && arg2==ZERO) return POS;**
**    ****if (arg1==POS  && arg2==POS)  return POS;**
**    ****return Bandera.choose(7);**
**    ****/* case (POS,NEG), (NEG,POS) */**
**  ****}**

**Notes:**
BASL specification are compiled into Java classes

For example, this is the Java class for the signs abstraction.

Abstract tokens are implemented as integer values.

The abstract function is straightforward.

And this is the definition of method add that implements the abstract version of +
-> we use a special method Bandera.choose the model the imprecision introduced by the abs.
-> For ex, Bandera.choose (7) will be interpreted in subsequent verification tools (i.e. JPF) as a non-deterministic    choice between the tokens encoded in the bit-vector 7, that is between NEG, ZERO, POS. 

## Data Type Abstractions

**Library of abstractions for base types contains:**
**Range(*****i,j*****)****,**** *****i..j***** modeled precisely, e.g., Range(0,0) is the *****signs***** abstraction**
**Modulo(k)****, ****Set(v,...)**
**Point**** maps all concrete values to ****unknown**
**User extendable for base types**
**Array abstractions**
**Specified by an index abstraction and an element abstraction**
**Class abstractions**
**Specified by abstractions for each field  **

## Comparison to Related Work 

**Predicate abstraction (Graf, Saidi)**
**We use PVS to abstract operator definitions, not complete systems**
**We can reuse abstractions for different systems**
**Tool support for program abstraction **
**e.g., SLAM, JPF, Feaver**
**Abstraction at the source-code level**
**Supports multiple checking tools **
**e.g., JPF, Java Checker/Verisoft, FLAVERS/Java, ...**

## Outline of the Talk

**Introduction**
**Data Abstraction**
**Program Completion (FSE’98, SPIN’99)**
**Abstract Counter-example Analysis**
**Formal Justification**
**Case Studies: Java and Ada Programs**
**Conclusions, Limitations and Future Work**

**Notes:**
Instead of analyzing the counter-ex for feasibility, we re-run Java Path Finder to do a customized search for feasible counter-examples on the fly, during verification of the abstracted program.
This resulted in a ...... 

## Program Completion 

**Software systems are collections of software ****components**
**Approach similar to unit testing of software**
**Applied to components (units) that are code complete**
**Stubs and drivers simulate ****environment**** for unit**
**We complete a system with a ****source code**** representation for missing components**
**Universal environments**
**Environment assumptions used to refine definitions of missing components**

**Notes:**
We want to reason about software components using tools that reason about complete systems

## procedure stub is
  choice: Integer;
  theObject: Object_Type;
 begin loop 
  case choice is
    when 1 => Insert(theObject);
    when 2 => theObject:=Remove;
    when 3 => null;
    when others => exit;
  end case; end loop; end stub;

**procedure stub is**
**  ****choice: Integer;**
**  ****theObject: Object_Type;**
** ****begin loop **
**  ****case choice is**
**    ****when 1 => ****Insert****(theObject);**
**    ****when 2 => theObject:=****Remove****;**
**    ****when 3 => null;**
**    ****when others => exit;**
**  ****end case; end loop; end stub;**

- Example of Universal Environment

**The stub for an Ada partial program, with an ****Insert ****procedure and a ****Remove**** ****function**

**Notes:**
Assumption: encapsulated; only properties of the partial system, not of the environment

## Assume-guarantee Model Checking

**A system specification is a pair <********>**
** ******** ****describes the property of the system**
** ******** ****describes the assumption about the environment**

**Notes:**
Problem definition
Implementation, Effective in practice
Experiments: our experience shows that synthesized environments enable faster verification
Comparison: assumptions encoded into the formula vs. encoded into the model

## Synthesis of Environments

**Environment assumptions ******
**Encode behavioral info. about system interfaces**
**Written in LTL**
**“****Classical” tableau construction for LTL**
**Modified to assume that only one interface operation can occur at a time**
**Builds a ****model**** of ********: **
**I.e., a graph with arcs labeled by interface operations**
**Can be easily translated into source code**

## Graph Generated from Assumption:

**(! Remove) U Insert**

**Notes:**
Safety, liveness
fairness

## Synthesized Code

**procedure stub is**
**  ****state,choice: Integer;**
**  ****theObject: Object_Type;**
**begin state:=0;**
** ****loop **
** ****case state is**
**  ****when 0 => case choice is**
**   ****when 1 => Insert(theObject);state:=8;**
**   ****when 2 => null;state:=9;**
**   ****when others => exit;**
**   ****end case;**
**  ****when 8 => case choice is**
**   ****when 1 => Insert(theObject);state:=8;**
**   ****when 2 => theObject:=Remove;state:=16;**
**   ****when 3 => null; state:=8;**
**   ****when others => exit;**
**   ****end case;**

**when 9 => case choice is**
** ****when 1 => Insert(theObject);state:=8;**
** ****when 2 => null;state:=9;**
** ****when others => exit;**
** ****end case;**
**when 16=> case choice is**
** ****when 1 => Insert(theObject);state:=16;**
** ****when 2 => theObject:=Remove;state:=16;**
** ****when 3 => null; state:=16;**
** ****when others => exit;**
** ****end case; **
**end case; end loop; end stub;**

## Comparison to Related Work 

**Much theoretical work on compositional verification**
**Avrunin, Dillon, Corbett: **
**Analysis of real-time systems, described as a mixture of source code and specifications**
**Colby, Godefroid, Jagadeesan: **
**Automatable approach to complete a partially specified system**
**Use the VeriSoft toolset**
**No environment assumptions**
**Long:**
**Synthesis of environments from ACTL**

## Outline of the Talk

**Introduction**
**Data Abstraction**
**Program Completion**
**Abstract Counter-example Analysis (TACAS’01)**
**Formal Justification**
**Case Studies: Java and Ada Programs**
**Conclusions, Limitations and Future Work**

**Notes:**
Instead of analyzing the counter-ex for feasibility, we re-run Java Path Finder to do a customized search for feasible counter-examples on the fly, during verification of the abstracted program.
This resulted in a ...... 

## Abstract Counter-example Analysis

**Example:**
**x = -2;     if(x + 2 == 0) then ...**
**x = NEG; if(Signs.eq(Signs.add(x,POS),ZERO)) then ...**
**                             ****{NEG,ZERO,POS}**

**For an abstracted program, a counter-example may be infeasible because:**
**Over-approximation introduced by abstraction**

**Notes:**
-> abs.program has more behaviors than the original program 

-> a counter-ex may be reported for a behavior in the abstract system not present in the original system

We developed a technique that searches for feasible counter-ex, during verification of the abstract system.  

## 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

## 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 include instructions that introduce non-determinism**
**JPF model checker modified**
**to detect non-deterministic choice (i.e. calls to ****Bandera.choose()****); backtrack from those points**

## Choice-bounded Search

** ****choose()**

**X**

**X**

**Notes:**
Verif. on choose free paths will report this path....

But not this paths.....

That may correspond to a feasible execution and indicates a real defect

## 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**

## Comparison to Related Work

**Previous work:**
**After model checking; analyze the counter-example to see if it is feasible**
**Pre-image computations; theorem prover based (InVest)**
**Forward simulation (CMU)**
**Symbolic execution (SLAM)**

**Notes:**
compare with previous work
 say what are these observations
Experience with defective Java applications
Our techniques could be combined with other approaches to obtain better results

## Outline of the Talk

**Introduction**
**Data Abstraction**
**Program Completion**
**Abstract Counter-example Analysis**
**Formal Justification**
**Case Studies: Java and Ada Programs**
**Conclusions, Limitations and Future Work**

**Notes:**
Instead of analyzing the counter-ex for feasibility, we re-run Java Path Finder to do a customized search for feasible counter-examples on the fly, during verification of the abstracted program.
This resulted in a ...... 

## Formal Justification

**Our techniques build ****safe abstractions**** of software systems**
**	****	****	****P < P’**** means “ P’ is a safe abstraction of P”**
**<**** is a ****simulation ****relation (Milner)**
**Properties are expressed**** ****in universal temporal logics (LTL, ACTL) preserved by ****<**

**Data Abstraction builds abstractions ****P****abs**** of systems ****P**** s.t.**** **
**	****	****	****P < Pabs**

**Universal Environments ****U****:**
**	****	****	****P||E < P||U****, for all environments ****E**

**Synthesized Environments ****T******** from assumptions ********:**
**	****	****	****P||E < P||T********, for all environments ****E**** that satisfy ******

**Notes:**
Not presented: semantical foundations of data abstractions: program text + (small-step) operational semantics -> program model; abstract program model ...

Formal def of simulation relation
Formally prove that we build safe abstractions
Inference rules: why if we show that a property is true for an abstracted program closed with synth environments it implies that the property is true on the original program, under assumption

## Outline of the Talk

**Introduction**
**Data Abstraction**
**Program Completion**
**Abstract Counter-example Analysis**
**Formal Justification**
**Case Studies: Java and Ada Programs**
**Conclusions, Limitations and Future Work**

**Notes:**
Instead of analyzing the counter-ex for feasibility, we re-run Java Path Finder to do a customized search for feasible counter-examples on the fly, during verification of the abstracted program.
This resulted in a ...... 

## Case Studies

**Filter-based Model Checking of a Reusable Parameterized Programming Framework**** (FSE’98)**
**Ada implementation of the Replicated Workers Framework**
**Model Checking Generic Container Implementations**** (GP’98)**
**Ada implementations of generic data structures:**
**queue, stack and priority queue**

**Abstracted using data type abstraction**
**Completed with code for universal environments**
**Environments’ behavior refined based on LTL assumptions**
**We used the SPIN tool:**
**To check 8/5 properties; 5/3 required use of assumptions**
**To detect seeded errors**

**Notes:**
Complexity RWF:
Large number of possible execution orderings of program actions
Complexity GCI:
 Data structures and algorithms

## Case Studies (contnd.)

**Assume-guarantee Model Checking of Software: A Comparative Case Study ****(SPIN’99)**** **
**Ada implementations of software components:**
**The Replicated Workers Framework, the Generic Containers**
**The Gas Station, the Chiron Client**

**Out of 39 properties, 15 required use of assumptions**
**For < ******** ****,******** >, we compared two ways of completing systems:**
**Universal environment****: check ******** ****->**** ******** (LTL) **
**using SPIN**
**Synthesized environment from ************(LTL): check ******** (LTL/ACTL)  **
**using SPIN/SMV**
**Synthesized environments enable faster verification**

**Notes:**
Only some properties required assumptions, relatively few assumptions

## Case Studies (contnd.)

**Analysis of the Honeywell DEOS Operating System ****(NASA’00,ICSE’01)**
**A real time operating system for integrated modular avionics**
**Non-trivial concurrent program (1433 lines of code, 20 classes, 6 threads)**
**Written in C++, translated into Java and Promela**
**With a known bug**
**Verification of the system exhausted 4 Gigabytes of memory without completion**

**Abstracted using data type abstraction**
**Completed with code for**
**User threads that run on the kernel**
**A system clock and a system timer **
**Environments’ behavior refined based on LTL assumptions**
**Checked using JPF and SPIN**
**Defect detected using choice-bounded search**

**Notes:**
Only some properties required assumptions, relatively few assumptions

## Case Studies (contnd.)

**Finding Feasible Counter-examples when Model Checking Abstracted Java Programs**** (TACAS’01)**
**We applied the 2 counter-example analysis techniques to Java defective applications:**
**Remote agent experiment, Pipeline, Readers-Writers, DEOS**

**Both techniques are fast:**
**Choose-free search is depth-bounded**
**Cost of simulation depends on the length of the counter-example**
**Choose-free counter-examples ...**
**are common**
**are short **
**enable more aggressive abstraction**

**Notes:**
RAX (Remote agent experiment) – component extracted from an embedded spacecraft-control application
Pipeline – a generic framework for multi-threaded staged calculations
RWVSN (Readers Writers) 
DEOS

## Summary

**We integrated several technologies into a coherent methodology that enables FSV of complex, concurrent software systems**
**We developed technologies for...**
**Data type abstraction:**
**Enable non-experts to generate models that make FSV less costly**
**Facilities to define, select and generate abstracted programs**
**Program completion**
**Enable verification of properties of individual components, collections of components and entire systems**
**Take into account assumptions about environment behavior**
**Analysis of abstract counter-examples**
**Choose-free state space search**
**Counter-example guided simulation**
**We implemented and formalized these technologies**
**We evaluated them on extensive case studies (Ada and Java)**

**Notes:**
Assumptions: local and global

## Future Work

**Generalize choice-bounded search technique**
**CTL* model checking of abstracted programs**
**Extend abstraction support for objects**
**Heap abstractions ****to**** ****handle an unbounded number of dynamically allocated objects**
**Extend automation**
**Automated selection**** and ****refinement**** of abstractions based on counter-example analysis**

**Notes:**
Currently we are extending bandera in these directions and we plan to report on it in the future
Limitations: we don’t handle recursive procedures, an unbounded number of processes (use heap abstractions to handle this!)

## Conclusions

**Tool support for:**
**Abstraction of data domains**
**Program completion**
**Interpretation of counter-examples**
**... ****is essential for the verification of realistic software systems**
**Ensures the safety of the verification process**

**Notes:**
Currently we are extending bandera in both these directions and we plan to report on it in the future

## Array Abstractions

**Specified by:**
**an index abstraction and **
**an element abstraction**
**Example: ****WidgetInfo wi[k]**
**use ****signs**** for index**
**use some other abstraction for ****WidgetInfo**
**Abstracted array ****awi ****has 2 elements:**
**awi[zero]**** abstracts ****wi[0]**
**awi[pos]**** summarizes info about ****wi[1] ...wi[k]**

## Property Abstraction

- System Model

- Property

## Property Abstraction

**Properties are temporal logic formulas, written in ****negational normal form.**
**Abstract propositions ****under-approximate**** the truth of concrete propositions.**
**Examples:**
**Invariance property: **
**Abstracted to: **
**Invariance property: **
**Abstracted to:**