The Quest for Hidden Meaning: Unveiling the Mystery of Psalm 22
Delve into the profound symbolism of Psalm 22 and uncover the hidden message behind the reference to Jesus as a worm. Explore the significance of the Hebrew word "tolaath" and its representation in biblical prophecy, shedding light on the deeper meaning of this enigmatic verse.
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.
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
x = i; y = j; ? = 0 ? + ? = 0 while y!=0 do x = x-1; y = y-1; ? + ? = ? + ? No! Yes! if( i==j ) assert x==0 2
Heap Numerical Arrays delete init PLDI08-1 NECLA-2 d-swap delete-all init-nc PLDI08-2 NECLA-3 strcpy find init-p PLDI08-3 SVCOMP-1 strlen filter init-e PLDI08-4 SVCOMP-2 memcpy last 2darray synergy-1 SVCOMP-3 find reverse synergy-2 copy SVCOMP-4 find-n Strings TACAS06 copy-p monniaux append NECLA-1 copy-o nested 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. while( ???? ? 0 ) 3. Propose a random modification to ? 4. if cost decreased then accept 5. if cost increased then 6. with some probability accept anyway 7. return ? 10
0 if ? makes VCs valid if ? is not an invariant ???? ? = 1 Problems Throughput < 1000 iterations per second No incremental feedback 11
Given sets of concrete states G: some reachable states B: some bad states Z: some implications s b g I t ????(?) = ? ? ?(?) + ? ??(?) + ?,? ?? ? ?(?) + Incremental feedback Efficient to evaluate 12
Reachable state ?,? ? = true ? ? = false ? ? ? ? ? {?} Pair (?,?), ? ? ?(?) ? ? ? ? = true ? ? ? Bad state ?, ? ? = false ? ? = true assume P while B do S assert Q 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?? ?,??? ??,? 10 ?=1 10 ?=1 ? ?? Search space: ?=1 Transformations for MCMC: Update a ? Update a ? Update all ? ? and ? of a single inequality 15
Fluid updates abstraction of DDA (ESOP10) ?,?.? ?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 Lding, 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, Kwangkeun Yi: 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
