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

© Copyright 2020