cav14 - Stanford University

Rahul Sharma and Alex Aiken (Stanford University)
1
x = i;
y = j;
while y!=0 do
x = x-1;
y = y-1;
if( i==j )
assert x==0


=0
+ =0
⋮

+ =+


No!
Yes!
2
Numerical
Arrays
Heap
delete
PLDI08-1
NECLA-2
init
d-swap
delete-all
PLDI08-2
NECLA-3
init-nc
strcpy
find
PLDI08-3
SVCOMP-1
init-p
strlen
filter
PLDI08-4
SVCOMP-2
init-e
memcpy
last
synergy-1
SVCOMP-3
2darray
find
reverse
synergy-2
SVCOMP-4
copy
find-n
TACAS06
monniaux
copy-p
append
Strings
NECLA-1
nested
copy-o
merge
length
reverse
alloc-f
replace
swap
alloc-nf
index
substring
3
assume P
while B do
S
assert Q

Find  that satisfies

⇒

 ∧   {}

 ∧ ¬ ⇒ 
Find a valuation of unknown predicates that
makes the verification conditions (VCs) valid
4

Given a set  of candidates
 Goal is to find a candidate that satisfies the VCs

This problem is hard!

Effective domain specific approaches
 Numerical, arrays, linked lists, etc.
Is it possible to have a general search procedure?
5

(Domain-specific) Checker + (General) Search = Inference

To obtain an invariant inference engine
 Instantiate the search with a search space
 An SMT solver to check
6

A generally applicable randomized search

Numerical, array, linked lists, and strings

Competitive performance with specialized approaches
7

Markov Chain Monte Carlo (MCMC) sampling

The only known tractable solution method for high
dimensional irregular search spaces [andrieu
03][chenney 00]
8
37
73
47
17
29
42
23
9
1.
2.
3.
4.
5.
6.
7.
 ≔ 
while(   ≠ 0 )
Propose a random modification to 
if cost decreased then accept
if cost increased then
with some probability accept anyway
return 
10

  =

Problems
0
1
if  makes VCs valid
if  is not an invariant
 Throughput < 1000 iterations per second
 No incremental feedback
11

Given sets of concrete states
 G: some reachable states
 B: some bad states
b
g
 Z: some implications

() =
∈ ¬()
∈ ()
,
…
+
s
I
t
Incremental feedback
+
∈   ∧ ¬() +
Efficient to evaluate
12

⇒

Reachable state ,   = true
   = false

 ∧   {}


   ∧ ¬  = true
 ∧ ¬ ⇒ 
assume P
while B do
S
assert Q
Pair (, ),   ⇒ ()

Bad state ,   = false
   = true
13

Given G, Z, and B, for the cost function

Run search until a 0-cost candidate  is found

ℎ , 
 SMT solver checks that  satisfies all the VCs
 If yes, then done

Update G, Z, or B and repeat
 SMT solvers can generate counterexamples
 If not then generate from executions
14

Program has integral variables 1 … 

Search space:

Transformations for MCMC:
10
=1
10
=1
,


=1  
≤ ,
 Update a 
 Update a 
 Update all  ′  and  of a single inequality
15
16
17

Fluid updates abstraction of DDA (ESOP’10)
 ∀, .  1 , … ,  , ,  ⇒   = []

Z3 fails to generate counterexamples

MCMC on this search space times out on ~30%
 Restrict search space: handle each in under a second
18

Search space: Boolean combinations of atoms
 Atoms are relations (1 , … ,  )
 Reachability relations

Use EPR (CAV’13) for check
19

Operations that intermix strings and integers
 length(s), indexOf(s1, s2), substr(s1, i1, i2), …

Search space: Boolean combinations of predicates

Z3-Str (FSE’13) for check
20

Static invariant inference is a hard problem,
made easier by separating search and check

Search based techniques can work
 Competitive with other methods
 Easier to retarget to new domains

Future work, scale MCMC to full program proofs
21

Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider: ICE: A Robust
Framework for Learning Invariants. CAV 2014

Shachar Itzhaky, Nikolaj Bjørner, Thomas W. Reps, Mooly Sagiv, Aditya V. Thakur:
Property-Directed Shape Analysis. CAV 2014

Rajeev Alur, Rastislav Bodík, Garvit Juniwal, Milo M. K. Martin, Mukund
Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina
Torlak, Abhishek Udupa: Syntax-guided synthesis. FMCAD 2013

Ashutosh Gupta, Rupak Majumdar, Andrey Rybalchenko: From tests to proofs.
STTT 15(4) (2013)

Yungbum Jung, Soonho Kong, Bow-Yaw Wang, KwangkeunYi:
Deriving Invariants by Algorithmic Learning, Decision Procedures,
and Predicate Abstraction. VMCAI 2010

Sumit Gulwani, Nebojsa Jojic: Program verification as probabilistic
inference. POPL 2007: 277-289
22