Software Verification Using SMT - Part II

smt and its application in software verification n.w
1 / 93
Embed
Share

Explore the application of Satisfiability Modulo Theories (SMT) in software verification through lazy abstraction and CFG unwinding. This detailed presentation covers examples, control-flow graphs, and computational processes to enhance understanding and practical implementation in software development.

  • Software Verification
  • SMT Application
  • Lazy Abstraction
  • Control-Flow Graphs
  • CFG Unwinding
rayaanacharya
jens_82 Follow

Uploaded on | 0 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.

Download Presentation

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.

E N D

Presentation Transcript

  1. SMT and Its Application in Software Verification (Part II) Yu-Fang Chen IIS, Academia Sinica Based on the slides of Barrett, Sanjit, Kroening , Rummer, Sinha, Jhala, and Majumdar, McMillan

  2. Lazy abstraction -- an example do{ L=0 lock(); old = new; if(*){ unlock(); new++; } } while (new != old); [L!=0] L=1; old=new L=0; new++ [new!=old] [new==old] control-flow graph program fragment

  3. Unwinding the CFG T 0 L=0 [L!=0] L=1; old=new L=0; new++ [new!=old] [new==old] control-flow graph

  4. Unwinding the CFG T 0 L=0 L=0 [L!=0] T 1 L=1; old=new Replace all free occurrences of L in the formula with L L=0; new++ [new!=old] [new==old] Compute Post (T, L=0)= T[L/L ] L=0[L/L ] = (L=0) control-flow graph Make Abstraction (L=0) T Pass

  5. Unwinding the CFG T 0 L=0 L=0 [L!=0] T [L!=0] 2 1 L=1; old=new Compute Post (T, [L!=0])= T (L!=0) L=0; new++ [new!=old] = (L!=0) ERROR state reached! [new==old] control-flow graph

  6. Unwinding the CFG T 0 L=0 L=0 [L!=0] T [L!=0] 2 1 L=1; old=new Compute Post (T, [L!=0])= T (L!=0) L=0; new++ [new!=old] = (L!=0) ERROR state reached! [new==old] T [L!=0] L=0 control-flow graph T L=0 L!=0

  7. Unwinding the CFG T 0 L=0 L=0 [L!=0] T [L!=0] 2 1 L=1; old=new Compute Post (T, [L!=0])= T (L!=0) L=0; new++ [new!=old] = (L!=0) ERROR state reached! [new==old] T [L!=0] L=0 control-flow graph T L=0 L!=0 WPre(L!=0, [L!=0]) = (L!=0) L!=0

  8. Unwinding the CFG T 0 L=0 L=0 [L!=0] T [L!=0] 2 1 L=1; old=new Compute Post (T, [L!=0])= T (L!=0) L=0; new++ [new!=old] = (L!=0) ERROR state reached! [new==old] L=0 [L!=0] L=0 control-flow graph T L=0 L!=0 Compute Craig Interpolant: (L=0) 1. (L=0) (L=0) 2. (L=0) (L=0) is UNSAT 3. Use only share var. of (L=0) and (L!=0) WPre(L!=0, [L!=0]) = (L!=0) L!=0

  9. Unwinding the CFG T 0 L=0 L=0 [L!=0] F L=0 [L!=0] 2 1 L=1; old=new Compute Post (T, [L!=0])= T (L!=0) L=0; new++ [new!=old] = (L!=0) ERROR state reached! [new==old] L=0 [L!=0] L=0 control-flow graph T L=0 L!=0 Compute Craig Interpolant: (L=0) 1. (L=0) (L=0) 2. (L=0) (L=0) is UNSAT 3. Use only share var. of (L=0) and (L!=0) WPre(L!=0, [L!=0]) = (L!=0) L!=0

  10. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new 3 L!=0 L=0; new++ [new!=old] Compute Post (L=0, L=1) = (L=0)[L/L ] L=1[L/L ] = (L =0 L=1) Compute Post (L =0 L=1, old=new) = (L =0 L=1)[old/old ] old=new[old/old ] = L =0 L=1 old=new Make Abstraction (L =0 L=1 old=new) (L!=0) Pass (L =0 L=1 old=new) (L=0) Not Passed [new==old] control-flow graph

  11. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new 3 L!=0 L=0; L=0; new++ new++ [new!=old] L=0 4 [new==old] Compute Post (L!=0, L=0) = (L!=0)[L/L ] L=0[L/L ] = (L !=0 L=0) Compute Post (L !=0 (L=0), new=new+1) = (L !=0 L=0)[new/new ] new=(new+1)[new/new ] = (L !=0 L=0 new=new +1) Make Abstraction (L !=0 L=0 new=new +1) (L!=0) Not Passed (L !=0 L=0 new=new +1) (L=0) Pass control-flow graph

  12. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new 3 L!=0 L=0; L=0; new++ new++ [new!=old] L=0 4 [new!=old] [new==old] L=0 5 Compute Post (L=0, [new!=old]) = (L=0 new!=old) Make Abstraction (L=0 new!=old) (L!=0) Not Passed (L=0 new!=old) (L=0) Pass control-flow graph

  13. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new 3 L!=0 L=0; L=0; new++ new++ [new!=old] L=0 4 [new!=old] [new==old] L=0 5 control-flow graph Covering: state 5 is subsumed by state 1. L=1 L=1 Pass

  14. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new 3 L!=0 L=0; L=0; new++ new++ [new!=old] L=0 4 [new!=old] [new==old] [new==old] L=0 L=0 5 7 Compute Post (L=0, [new==old]) = (L=0 new==old) Make Abstraction (L=0 new!=old) (L!=0) Not Passed (L=0 new!=old) (L=0) Pass control-flow graph

  15. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new 3 L!=0 L=0; L=0; new++ new++ [new!=old] L!=0 L=0 4 8 [new!=old] [new==old] [new==old] L=0 L=0 5 7 No Actions control-flow graph

  16. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new 3 L!=0 L=0; L=0; new++ new++ [new!=old] L!=0 L=0 4 8 [new!=old] [new==old] [new==old] [new==old] L=0 L=0 5 7 9 L!=0 control-flow graph Compute Post (L!=0, [new==old]) = (L!=0 new==old) Make Abstraction (L!=0 new==old) (L!=0) Pass (L!=0 new==old) (L=0) Not Passed

  17. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new 3 L!=0 L=0; L=0; new++ new++ [new!=old] L!=0 L=0 4 8 [new!=old] [new!=old] [new==old] [new==old] [new==old] L=0 L=0 10 5 7 9 L!=0 L!=0 control-flow graph Compute Post (L!=0, [new!=old]) = (L!=0 new!=old) Make Abstraction (L!=0 new!=old) (L!=0) Pass (L!=0 new!=old) (L=0) Not Passed

  18. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new 3 L!=0 L=0; L=0; new++ new++ [new!=old] L!=0 L=0 4 8 [new!=old] [new!=old] [new==old] [new==old] [new==old] L=0 [L!=0] L=0 10 5 7 9 11 L!=0 L!=0 control-flow graph Compute Post (L!=0, [L!=0]) = (L!=0 L!0) ERROR state reached!

  19. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new 3 L!=0 L=0; L=0; new++ new++ [new!=old] L!=0 L=0 4 8 [new!=old] [new!=old] [new==old] [new==old] [new==old] L=0 [L!=0] L=0 10 5 7 9 11 L!=0 L!=0 control-flow graph L!=0 L!=0 L!=0 L=0 L=1 old=new L =0 L=1 old=new L=0 [L!=0] [new!=old] L!=0 old!=new T L=0 L!=0 L!=0

  20. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new 3 L!=0 L=0; L=0; new++ new++ [new!=old] L!=0 L=0 4 8 [new!=old] [new!=old] [new==old] [new==old] [new==old] L=0 [L!=0] L=0 10 5 7 9 11 L!=0 L!=0 control-flow graph L!=0 L!=0 L!=0 L=0 L=1 old=new L =0 L=1 old=new L=0 [L!=0] [new!=old] L!=0 old!=new T L=0 L!=0 L!=0 L!=0 old!=new L!=0

  21. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new 3 L!=0 L=0; L=0; new++ new++ [new!=old] L!=0 L=0 4 8 [new!=old] [new!=old] [new==old] [new==old] [new==old] L=0 [L!=0] L=0 10 5 7 9 11 L!=0 L!=0 control-flow graph L!=0 L!=0 L!=0 L=0 L=1 old=new L =0 L=1 old=new L=0 [L!=0] [new!=old] L!=0 old!=new T L=0 L!=0 L!=0 L!=0 old!=new L!=0 L!=0 old!=new L!=0 old!=new

  22. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new 3 L!=0 L=0; L=0; new++ new++ [new!=old] L!=0 L=0 4 8 [new!=old] [new!=old] [new==old] [new==old] [new==old] L=0 [L!=0] L=0 10 5 7 9 11 L!=0 L!=0 control-flow graph L!=0 L!=0 L!=0 L=0 L=1 old=new L =0 L=1 old=new L=0 [L!=0] [new!=old] L!=0 old!=new T L=0 L!=0 L!=0 L!=0 L!=0 old!=new L!=0 old!=new L!=0 old!=new

  23. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new L!=0 old =new 3 L=0; L=0; new++ new++ [new!=old] L!=0 L=0 4 8 [new!=old] [new!=old] [new==old] [new==old] [new==old] L=0 [L!=0] L=0 10 5 7 9 11 L!=0 L!=0 control-flow graph L!=0 L!=0 L=0 L!=0 old=new L=1 old=new L =0 L=1 old=new L=0 [L!=0] [new!=old] L!=0 old!=new T L=0 L!=0 L!=0 L!=0 L!=0 old!=new L!=0 old!=new L!=0 old!=new

  24. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new Remove all of its children L!=0 old =new 3 L=0; L=0; new++ new++ [new!=old] L!=0 L=0 4 8 [new!=old] [new!=old] [new==old] [new==old] [new==old] L=0 [L!=0] L=0 10 5 7 9 11 L!=0 L!=0 control-flow graph L!=0 L!=0 L=0 L!=0 old=new L=1 old=new L =0 L=1 old=new L=0 [L!=0] [new!=old] L!=0 old!=new T L=0 L!=0 L!=0 L!=0 L!=0 old!=new L!=0 old!=new L!=0 old!=new

  25. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new L!=0 old =new 3 L=0; new++ [new!=old] [new==old] control-flow graph

  26. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new L!=0 old =new 3 L=0; L=0; new++ new++ [new!=old] L=0 old !=new 4 [new==old] Compute Post (L!=0 old =new, L=0) = (L!=0 old=new)[L/L ] L=0[L/L ] = (L !=0 old=new L=0) Compute Post (L !=0 old=new (L=0), new=new+1) = (L !=0 old=new L=0)[new/new ] new=(new+1)[new/new ] = (L !=0 old=new L=0 new=new +1) Make Abstraction (L !=0 old=new L=0 new=new +1) (L!=0) Not Passed (L !=0 old=new L=0 new=new +1) (L=0) Pass (L !=0 old=new L=0 new=new +1) (old=new) Not Passed (L !=0 old=new L=0 new=new +1) (old!=new) Pass control-flow graph

  27. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new L!=0 old=new 3 L=0; L=0; new++ new++ [new!=old] L=0 old =new 4 [new!=old] [new==old] L=0 old!=new 5 Compute Post (L=0 old!=new, [new!=old]) = (L=0 new!=old) Make Abstraction (L=0 new!=old) (L!=0) Not Passed (L=0 new!=old) (L=0) Pass (L=0 new!=old) (old=new) Not Passed (L=0 new!=old) (old!=new) Pass control-flow graph

  28. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new L!=0 old=new 3 L=0; L=0; new++ new++ [new!=old] L=0 old =new 4 [new!=old] [new==old] L=0 old!=new 5 control-flow graph Covering: state 5 is subsumed by state 1. L=1 old!=new L=1 Pass

  29. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new L!=0 old=new 3 L=0; L=0; new++ new++ [new!=old] L=0 old =new 4 [new!=old] [new==old] [new==old] L=0 old=new 5 7 L=0 old!=new Compute Post (L=0, [new==old]) = (L=0 new=old) Make Abstraction (L=0 new=old) (L!=0) Not Passed (L=0 new=old) (L=0) Pass (L=0 new=old) (new!=old) Not Passed (L=0 new=old) (new=old) Pass control-flow graph

  30. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new L!=0 old=new 3 L=0; L=0; new++ new++ [new!=old] L!=0 old=new L=0 old =new 4 8 [new!=old] [new==old] [new==old] 5 7 L=0 old!=new L=0 old=new No Actions control-flow graph

  31. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new L!=0 old=new 3 L=0; L=0; new++ new++ [new!=old] L!=0 old=new L=0 old =new 4 8 [new!=old] [new==old] [new==old] [new==old] 9L!=0 old=new 5 7 L=0 old!=new L=0 old=new control-flow graph Compute Post (L!=0 new=old, [new==old]) = (L!=0 new=old) Make Abstraction (L!=0 new=old) (L!=0) Pass (L!=0 new=old) (L=0) Not Passed (L!=0 new=old) (old=new) Pass (L!=0 new=old) (old!=new) Not Passed

  32. Unwinding the CFG T 0 L=0 L=0 [L!=0] F [L!=0] L=0 2 1 L=1; old=new L=1; old=new L!=0 old=new 3 L=0; L=0; new++ new++ [new!=old] L!=0 old=new L=0 old =new 4 8 [new!=old] [new!=old] [new==old] [new==old] [new==old] 10 9L!=0 old=new 5 7 F L=0 old!=new L=0 old=new control-flow graph Compute Post (L!=0 new=old, [new!=old]) = (L!=0 new=old new!=old ) = false

  33. Another Approach: The IMPACT method Kenneth L. McMillan: Lazy Abstraction with Interpolants. CAV 2006: 123-136 33

  34. (Craig,57) Interpolation Lemma

  35. (Craig,57) Interpolation Lemma Notation: L( ) is the set of FO formulas over the symbols of

  36. (Craig,57) Interpolation Lemma Notation: L( ) is the set of FO formulas over the symbols of If A B = false, there exists an interpolant A' for (A,B) such that: A A' A' B = false A' 2 L(A) L(B)

  37. (Craig,57) Interpolation Lemma Notation: L( ) is the set of FO formulas over the symbols of If A B = false, there exists an interpolant A' for (A,B) such that: A A' A' B = false A' 2 L(A) L(B) Example: A = p q, B = q r, A' = q

  38. (Craig,57) Interpolation Lemma Notation: L( ) is the set of FO formulas over the symbols of If A B = false, there exists an interpolant A' for (A,B) such that: A A' A' B = false A' 2 L(A) L(B) Example: A = p q, B = q r, A' = q Interpolants from proofs in certain quantifier-free theories, we can obtain an interpolant for a pair A,B from a refutation in linear time. [McMillan 05] in particular, we can have linear arithmetic,uninterpreted functions, and restricted use of arrays

  39. Interpolants for sequences

  40. Interpolants for sequences Let A1...Anbe a sequence of formulas

  41. Interpolants for sequences Let A1...Anbe a sequence of formulas A sequence A 0...A nis an interpolant for A1...Anwhen

  42. Interpolants for sequences Let A1...Anbe a sequence of formulas A sequence A 0...A nis an interpolant for A1...Anwhen A 0= True

  43. Interpolants for sequences Let A1...Anbe a sequence of formulas A sequence A 0...A nis an interpolant for A1...Anwhen A 0= True A i-1 Ai) A i, for i = 1..n

  44. Interpolants for sequences Let A1...Anbe a sequence of formulas A sequence A 0...A nis an interpolant for A1...Anwhen A 0= True A i-1 Ai) A i, for i = 1..n An= False

  45. Interpolants for sequences Let A1...Anbe a sequence of formulas A sequence A 0...A nis an interpolant for A1...Anwhen A 0= True A i-1 Ai) A i, for i = 1..n An= False and finally, A i2 L (A1...Ai) L(Ai+1...An)

  46. Interpolants for sequences Let A1...Anbe a sequence of formulas A sequence A 0...A nis an interpolant for A1...Anwhen A 0= True A i-1 Ai) A i, for i = 1..n An= False and finally, A i2 L (A1...Ai) L(Ai+1...An) ... A1 A2 A3 Ak

  47. Interpolants for sequences Let A1...Anbe a sequence of formulas A sequence A 0...A nis an interpolant for A1...Anwhen A 0= True A i-1 Ai) A i, for i = 1..n An= False and finally, A i2 L (A1...Ai) L(Ai+1...An) ... A1 A2 A3 Ak True False ... ) ) ) ) ) ) ) ) A'1 A'2 A'3 A'k-1

  48. Interpolants for sequences Let A1...Anbe a sequence of formulas A sequence A 0...A nis an interpolant for A1...Anwhen A 0= True A i-1 Ai) A i, for i = 1..n An= False and finally, A i2 L (A1...Ai) L(Ai+1...An) ... A1 A2 A3 Ak True False ... ) ) ) ) ) ) ) ) A'1 A'2 A'3 A'k-1 In other words, the interpolant is a structured refutation of A1...An

  49. Interpolants as Floyd-Hoare proofs

  50. Interpolants as Floyd-Hoare proofs x=y; y++; [x=y]

Related


No related presentations.

More Related Content