A Data-Driven Approach for Algebraic Loop Invariants
This research delves into algebraic loop invariants, showcasing a methodical process for deriving, refining, and validating these crucial components in program analysis. The approach employs data generation, processing, and null space exploration to infer robust invariants, demonstrating the value of combining theoretical principles with practical data-driven techniques.
Uploaded on Mar 09, 2025 | 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.
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
A Data Driven Approach for Algebraic Loop Invariants Rahul Sharma Joint work with Saurabh Gupta, Bharath Hariharan, Alex Aiken, Percy Liang, and Aditya Nori (UC Berkeley, Stanford, Microsoft Research India)
Algebraic invariants Consider a program Over variables ? (?1, ,??) assume ?( ?); while B do S Algebraic invariant ?( ?) ?(?? ? = 0) ? ? ? ? ?{?}
Example program assume x = y = 0; while( * ) { y := y+1; x := x+y; } ? = 0 ? = 0 ? ? ? = ? + 1;? = ? + ?{?} Target invariant Strongest invariant Of a given degree d d=2, 2? = ? ? + 1 d=1, ????
Guess-and-Check (G&C) Generate data at the desired program point Guess a candidate invariant (Linear Algebra) Check whether candidate is an actual invariant If not, guess again
Data generation Execute programs to generate data assume x = y = 0; while( * ) { Print(x,y); y := y+1; x := x+y; } x y 0 0 1 1 3 2 6 3
Data processing Given degree = 2 ? + ?? + ?? + ??2+ ??2+ ??? = 0 1 x y x^2 y^2 xy x y 1 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 3 2 9 4 6 3 2 1 6 3 36 9 18 6 3 Data Matrix (?): One column for each monomial
Null space for candidate invariants ????????? ? = ? ?? = 0} All such vectors ? can be represented by basis ? b1 b2 1 x y x^2 y^2 xy 0 0 0 1 0 0 0 0 0 0 -2 -9 1 1 1 1 1 1 0 1 3 2 9 4 6 1 6 1 6 3 36 9 18 0 0 -1 0 1 0 0 0 1
Invariants are in null space ? 2? = ? + ?2,? = [0, 2,1,0,1,0] Each algebraic equation of the target invariant Satisfies data Aw = 0 b1 b2 0 0 ? is basis of null space, ? generates ? -2 -9 1 6 ? = 1 ?1+ 0 ?2 0 -1 1 0 0 1
Sound under-approximation Candidate ?: 2? = ? + ?2 9? + ?2= 6?2+ ?? ? 2? = ? + ?2 Using, invariant lies in null space of data matrix and, candidate captures null space, we conclude, ? ? Lack of data leads to spurious equations Candidate captures all equalities consistent with data
Check phase ?:2? = ? + ?2 9? + ?2= 6?2+ ?? ? = 0 ? = 0 ? ? ? = ? + 1;? = ? + ? ? Fails, 6,3 ? = ? + 1;? = ? + ?{ 10,4 } Add (10,4) to ? New candidate, 2? = ? + ?2
Guess-and-Check (summary) Run tests and print states at the loop head 1. Create data matrix ? using the given degree 2. Guess a candidate invariant using ?????????(?) If ? is empty, return ????? If null space is zero-dimensional, return ???? 3. Check whether candidate is an actual invariant If yes, then done If no, then add counter-example to ?, and goto 3 4.
Soundness G&C terminates only if candidate is an invariant Need to prove that output is the strongest invariant Counter-examples satisfy the target invariant ? ?:2? = ? + ?2 9? + ?2= 6?2+ ?? ?:2? = ? + ?2 I C
Termination Counter-example violates candidate invariant It is linearly independent of the rows of ? Adding the counter-example increases rank by 1 Rank of data matrix is bounded by ?, #columns
Our Results Formally characterize candidate invariants ? ? Augment candidate generation with SMT Sound approach for inferring algebraic invariants Terminating procedure If checking terminates then so does inference
Consequences Starting with zero states in data matrix G&C terminates in at most ? iterations With strongest algebraic invariant Program tests decrease the number of G&C iterations
Nested Loops Instrument all loop heads, run whole program tests Generate candidate invariants for all loops Check them simultaneously: Inner loops replaced by candidates Candidates of outer loops generate preconditions For a program with ? loops and ? data matrix columns Terminate in ?2? iterations with algebraic invariants
Implementation MATLAB for computing null space Z3 for checking invariants Decision procedure queries in Peano arithmetic Generated tests naively Inputs within a small bounding box
Arrays (i,a[0]) = (0,0); assume (n > 0); while (i != n) { Print(i,a[i],n) i := i+1; a[i] := a[i-1]+1; } assert(a[n] == n); Mine equalities from data Create a column for what we want to relate 1 i a[i] n 1 0 0 1 1 1 1 1 1 0 0 2 ? ? ? = ?
Related Work Do not assume degree, but ignore nested loops Rodr guez-Carbonell and Kapur[07], Kov cs[09] Restrict branches to equalities or dis-equalities Sankaranarayanan et al.[04], M ller-Olm and Seidl[04], Col n[04], Rodr guez-Carbonell and Kapur[07] Does not use Gr bner bases: Cachera et al.[12] Unsound: Daikon, Nguyen et al.[12]
Conclusion Sound and terminating inference engine Data Driven: Leverage test suites for proofs Separation of guess and check phases Handle a rich syntax Conceptually simple Easy to engineer Future work: Guess and check for richer invariants
