BLAST

Information about BLAST

Published on January 16, 2008

Author: Reginaldo

Source: authorstream.com

Content

BLAST-A Model Checker for C:  BLAST-A Model Checker for C Developed by Thomas A. Henzinger (EPFL) Rupak Majumdar (UC Los Angeles) Ranjit Jhala (UC San Diego) Dirk Beyer (Simon Fraser University) Presented by Sowmya Venkateswaran BLAST Installation:  BLAST Installation Currently version 2.0 src files available. http://mtc.epfl.ch/software-tools/blast/ Installation Download Simplify theorem prover http://www.cs.virginia.edu/~weimer/615/hw.html Either build from src files or use Linux binaries. A “working” example configuration for compiling Blast 2.0 is OCaml 3.08.3 and gcc (GCC) 3.4.4 20050721 (Red Hat 3.4.4-2). Features:  Features “On the Fly” Abstraction Automatic abstraction Smarter predicate discovery Verify safety properties, assertion violations Finding reachable program locations Detecting dead code Reuse saved abstractions Problems:  Problems Installing and making it work Predicate discovery not good enough. Checking concurrent programs Eclipse plugin Checking recursive functions BLAST working:  BLAST working Build an abstract model using predicate abstraction. Check for reachability of a specified label using the abstract model. If no path to ERR node-system safe. If path is feasible, output error trace. Else use infeasibility of path to refine abstract model. BLAST working:  BLAST working CIL Infrastructure C Program Property spec.opt Instrumented C file with error label Lazy Abstraction CFA Forward Search Phase ART Error node unreachable; program safe Backward counterexample analysis Refine Add Predicates Problem: Abstraction is expensive:  Problem: Abstraction is expensive # of abstract states=2# of predicates Solution 1: Only abstract reachable states Solution 2: Don’t refine any error free states Advantages: State space only refined as much as required. Reuse previously defined error free states. Lazy Abstraction:  Lazy Abstraction Integrate the following Abstraction Verification Counterexample-driven refinement Find pivot state. Construct, verify and refine abstract model “on the fly” from pivot state on. Forward Search Phase and Backward Counterexample analysis. Stop when either real counterexample found or system found safe Locking example:  Locking example Control Flow Automaton:  Control Flow Automaton Local and global variables of C program Vertices: control locations of a function. Labeled directed edges Basic block of instructions. Assume predicate for branch condition. Formally, CFA is a tuple <Q,q0,X,Ops,→> Q- finite set of control locations q0-initial control location X- set of variables Ops- set of operations on X (lval=exp or [p]) →∈(Q x Ops x Q) Control Flow Automaton:  Control Flow Automaton Forward Search Phase:  Forward Search Phase Abstract reachability tree in dfs order. Constructed from CFA. Vertices in CFA are nodes in ART. Labels of nodes are reachable regions. Reachable region obtained from parent’s reachable region and instructions on the edge between them. Finite set of predicates per node. Reachable region is a boolean combination of set of predicates Forward Search for locking example:  Forward Search for locking example 1 LOCK=0 2 [T] LOCK=0 lock() old=new 3 LOCK=1 4 [T] LOCK=1 5 unlock() new++ LOCK=0 [new=old] 6 LOCK=0 unlock() ERR LOCK=0 Is this a valid counterexample?? Weakest Precondition:  Weakest Precondition WP(P,Op) –weakest formula P` s.t. if P` is T before Op, then P is T after Op Assign x=e P P [e / x ] new+1=old new=new + 1 new=old Weakest Precondition:  Weakest Precondition WP(P,Op) –weakest formula P` s.t. if P` is T before Op, then P is T after Op Assume [C] P C ^ P new = old [ new=old ] new=old Backward Counterexample Analysis:  Backward Counterexample Analysis For each tree node, find a bad region. Bad region of ERR node=T Other nodes=WP of bad region of child w.r.t instructions on edge between the 2. Start from ERR node Pivot node - First node in the tree where Bad region ∩ Reachable region=φ Refine abstraction from pivot node onwards Counter example analysis for locking program:  Counter example analysis for locking program 1 LOCK=0 2 [T] LOCK=0 lock() old=new 3 LOCK=1 4 [T] LOCK=1 5 unlock() new++ LOCK=0 [new=old] 6 LOCK=0 unlock() ERR LOCK=0 {LOCK=0} { LOCK=0 & new=old } { LOCK=1 & new+1=old } { LOCK=1 & new+1=old } { LOCK=0 & new+1=new } {T} Searching with new predicate new=old:  Searching with new predicate new=old 1 LOCK=0 2 [T] LOCK=0 3 LOCK=1 & new=old 4 5 LOCK=0& !new=old 2 6 5 2 6 [T] [T] [new!=old] LOCK=1 & new=old LOCK=1 & new=old [new=old] RET unlock() LOCK=0 & new=old False False LOCK=0 Program Safe!! Finding Predicates:  Finding Predicates Problem: How many predicates to find? # of predicates grows with program size 2n abstract states!! p1 p2 pn Solution: Use predicates only where needed 2n abstract states Counter example Traces:  Counter example Traces 1:x=ctr; 2:ctr=ctr+1; 3:y=ctr; 4: if (x=i-1) { 5: if (y!=i){ ERROR; }} 1: x=ctr; 2: ctr=ctr+1; 3: y=ctr; 4: assume (x=i-1) 5: assume (y!=i) Theorem: Trace formula is satisfiable iff trace is feasible. Counter example trace Sample program 1:x1=ctr0 2:ctr1=ctr0+1 3:y1=ctr1 4:x1=i0-1 5:y1!=i0 Trace Formula φ Trace formula is a conjunction of constraints, one per instruction in the trace. Steps in Refine Stage:  Steps in Refine Stage Counter example trace Trace formula Proof of Unsatisfiability Theorem Prover Interpolate Predicate Map Finding what predicates are needed:  Finding what predicates are needed 1: x=ctr; 2: ctr=ctr+1; 3: y=ctr; 4: assume (x=i-1) 5: assume (y!=i) 1:x1=ctr0 2:ctr1=ctr0+1 3:y1=ctr1 4:x1=i0-1 5:y1!=i0 What predicate is needed for trace to become infeasible Trace Trace Formula Given an infeasible trace t, find a set of predicates P, such that t is abstractly infeasible w.r.t P. Slide23:  Partition φ into φ- (trace prefix) and φ+ (trace suffix) Find an interpolant Ψ s.t φ- implies Ψ Ψ ^ φ+ is unsatisfiable. The variables of Ψ are common to both φ- and φ+ Use interpolant to construct predicate map. Finding what predicates are needed Interpolant = Predicate:  Interpolant = Predicate 1:x1=ctr0 2:ctr1=ctr0+1 3:y1=ctr1 4:x1=i0-1 5:y1!=i0 Trace Formula φ- φ+ Interpolate φ Predicate at 4: y=x+1 Predicate is ..implied by Trace formula prefix ..on common variables ..makes Trace Formula suffix unfeasible x1 y1 y1 x1 Finding predicate map:  Finding predicate map Partition at each point Interpolate at each partition Construct predicate map pci  Interpolant from partition i Trace Trace Formula 1: x=ctr; 2: ctr=ctr+1; 3: y=ctr; 4: assume (x=i-1) 5: assume (y!=i) 1:x1=ctr0 2:ctr1=ctr0+1 3:y1=ctr1 4:x1=i0-1 5:y1!=i0 φ- φ+ Interpolate x1=ctr0 Predicate Map 2: x1=ctr0 Slide26:  Partition at each point Interpolate at each partition Construct predicate map pci  Interpolant from partition i Trace Trace Formula 1: x=ctr; 2: ctr=ctr+1; 3: y=ctr; 4: assume (x=i-1) 5: assume (y!=i) 1:x1=ctr0 2:ctr1=ctr0+1 3:y1=ctr1 4:x1=i0-1 5:y1!=i0 φ- φ+ Interpolate x1=ctr1-1 Predicate Map 2: x1=ctr0 3: x1=ctr1-1 Finding predicate map Finding predicate map:  Finding predicate map Partition at each point Interpolate at each partition Construct predicate map pci  Interpolant from partition i Trace Trace Formula 1: x=ctr; 2: ctr=ctr+1; 3: y=ctr; 4: assume (x=i-1) 5: assume (y!=i) 1:x1=ctr0 2:ctr1=ctr0+1 3:y1=ctr1 4:x1=i0-1 5:y1!=i0 φ- φ+ Interpolate y1=x1+1 Predicate Map 2: x1=ctr0 3: x1=ctr1-1 4: y1=x1+1 Finding predicate map:  Finding predicate map Partition at each point Interpolate at each partition Construct predicate map pci  Interpolant from partition i Trace Trace Formula 1: x=ctr; 2: ctr=ctr+1; 3: y=ctr; 4: assume (x=i-1) 5: assume (y!=i) 1:x1=ctr0 2:ctr1=ctr0+1 3:y1=ctr1 4:x1=i0-1 5:y1!=i0 φ- φ+ Interpolate y1=i0 Predicate Map 2: x1=ctr0 3: x1=ctr1-1 4: y1=x1+1 5: y1=i0 BLAST Specification language:  BLAST Specification language Include directives Global variables Shadowed types Events Pattern Guard Action/Repair Before/After References:  References “Abstractions from Proofs”-Thomas .H et al. “The Blast query language for software verification”- Dirk Beyer et al. “Lazy Abstraction”-Gregoire Sutre et al.

Related presentations


Other presentations created by Reginaldo

fall construction
08. 01. 2008
0 views

fall construction

Maori Culture
10. 01. 2008
0 views

Maori Culture

3rdconf tonetti
11. 01. 2008
0 views

3rdconf tonetti

GoodFaith
13. 01. 2008
0 views

GoodFaith

2004 u apresentacao
13. 01. 2008
0 views

2004 u apresentacao

MetaRx
14. 01. 2008
0 views

MetaRx

pp4
15. 01. 2008
0 views

pp4

Quasi Newton
16. 01. 2008
0 views

Quasi Newton

Cultural Competence
17. 01. 2008
0 views

Cultural Competence

miracles gcse
17. 01. 2008
0 views

miracles gcse

AC Grad Presentation
18. 01. 2008
0 views

AC Grad Presentation

The Colonial Period
19. 01. 2008
0 views

The Colonial Period

farag
22. 01. 2008
0 views

farag

Georgia MRSA
23. 01. 2008
0 views

Georgia MRSA

khan
24. 01. 2008
0 views

khan

kelly
05. 02. 2008
0 views

kelly

TireFBCpowerpoint
12. 02. 2008
0 views

TireFBCpowerpoint

Backyard Biology
25. 01. 2008
0 views

Backyard Biology

statia pptreview1
28. 01. 2008
0 views

statia pptreview1

ER to REL
29. 01. 2008
0 views

ER to REL

Doctor Faustus
29. 01. 2008
0 views

Doctor Faustus

Event Planning Record 9
06. 02. 2008
0 views

Event Planning Record 9

ciforp
07. 02. 2008
0 views

ciforp

Yuan and Ming Dynasties
07. 02. 2008
0 views

Yuan and Ming Dynasties

MissionPossible
13. 02. 2008
0 views

MissionPossible

20050517 TCBACMeeting Process
14. 02. 2008
0 views

20050517 TCBACMeeting Process

SpiralDynamics IPGA
18. 02. 2008
0 views

SpiralDynamics IPGA

cs554 lect05
11. 01. 2008
0 views

cs554 lect05

NIHPCS1002f
24. 01. 2008
0 views

NIHPCS1002f

mandarin 103007
11. 03. 2008
0 views

mandarin 103007

AAMAS07 Invitation
14. 03. 2008
0 views

AAMAS07 Invitation

lahey9e 08
08. 02. 2008
0 views

lahey9e 08

2006 12 01 Roman
28. 03. 2008
0 views

2006 12 01 Roman

M6
09. 01. 2008
0 views

M6

Hurd IRAC
12. 01. 2008
0 views

Hurd IRAC

Applications January 2007v2
10. 04. 2008
0 views

Applications January 2007v2

maxine brown
16. 04. 2008
0 views

maxine brown

aegean
08. 03. 2008
0 views

aegean

200571816522254
18. 04. 2008
0 views

200571816522254

Gross Domestic Product vs
21. 04. 2008
0 views

Gross Domestic Product vs

2000 annual results analyst
22. 04. 2008
0 views

2000 annual results analyst

CERTUnit8
24. 04. 2008
0 views

CERTUnit8

Chap05
07. 05. 2008
0 views

Chap05

PPT RobertScollay
08. 05. 2008
0 views

PPT RobertScollay

Overview2006
05. 02. 2008
0 views

Overview2006

caring
30. 04. 2008
0 views

caring

8 09 15
02. 05. 2008
0 views

8 09 15

Abilene Metadata 2 20070919
03. 03. 2008
0 views

Abilene Metadata 2 20070919

491158BECB
02. 05. 2008
0 views

491158BECB

LT1053N 01 2007
04. 02. 2008
0 views

LT1053N 01 2007

Washingtons Presidency
22. 01. 2008
0 views

Washingtons Presidency

1 20080121100630
14. 04. 2008
0 views

1 20080121100630

mccrory
12. 03. 2008
0 views

mccrory

EHS Tech Update1 6 23 20041
09. 01. 2008
0 views

EHS Tech Update1 6 23 20041

FrancoisViruly
04. 02. 2008
0 views

FrancoisViruly

Hamburgpipe
14. 01. 2008
0 views

Hamburgpipe

Sercel
17. 01. 2008
0 views

Sercel

fg alt off learn sept 06
15. 01. 2008
0 views

fg alt off learn sept 06

1 800 MAR TIAN
24. 01. 2008
0 views

1 800 MAR TIAN

bergmann erf 1999
29. 02. 2008
0 views

bergmann erf 1999

YLemel Brno
07. 02. 2008
0 views

YLemel Brno

A Lamond Triton
11. 01. 2008
0 views

A Lamond Triton

Sarcoidosis 3
11. 02. 2008
0 views

Sarcoidosis 3

Bilanz Mediakomm Kraft
31. 01. 2008
0 views

Bilanz Mediakomm Kraft

BJA IED Mod1 IntrotoIED
11. 01. 2008
0 views

BJA IED Mod1 IntrotoIED

Vols of Yr Event 2006 26 Apr
04. 02. 2008
0 views

Vols of Yr Event 2006 26 Apr