Proving Program Termination Using Tests and Loops
Revealing the use of tests and loop structures for proving program termination, breaking down complex problems into manageable steps. Exploration of static techniques and neglected testing sources to exploit available information. Demonstrating the application through examples like the GCD algorithm and inferring loop iteration bounds based on inputs and loop attributes.
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
AdityaNori MSR India Stanford University Rahul Sharma
Prove termination of a program Program terminates if all loops terminate Hard problem, undecidable in general Need to exploit all available information
Previous techniques are static Tests are a neglected source of information Tests have previously been used Safety properties, empirical complexity, This work, use tests for termination proofs
gcd(int x,int y) assume(x>0 && y>0); while( x!=y ) do if( y > x ) y = y x; if( x > y) x = x-y; od return x; x=1, y=1 x=2, y=1
while while print x print y (1,1) (2,1) x=1, y=3 while assert Data ML
while while print x print y (1,1) (2,1) x=1, y=3 while assert Data ML
gcd(int x, int y) assume(x>0 && y>0); a := x; b := y; c := 0; while( x!=y ) do c := c + 1; if( y > x ) y := y x; if( x > y) x := x-y; od print ( a, b, c ); New variables to capture initial values Introduce a loop counter Print values of input variables and counter
while while print x print y (1,1) (2,1) x=1, y=3 while assert Data ML
? 0 1 2 gcd(int x, int y) assume(x>0 && y>0); a := x; b := y; c := 0; while( x!=y ) do c := c + 1; if( y > x ) y := y x; if( x > y) x := x-y; od print( a, b, c) 1 1 1 1 ? 1 2 1 ? 1 1 3 ? ? For ? , on inputs ??, the loop iterates ?? times Infer a bound using ? and ?
while while print x print y (1,1) (2,1) x=1, y=3 while assert Data ML
Predict number of iterations (final value ofc) As a linear expression in a and b Findw1,w2,w3:?1+ ?2??+ ?3?? ?? ? Findw1,w2,w3: min ?=1 2 ?1+ ?2??+ ?3?? ?? But we want?1+ ?2? + ?3? ? Add?1+ ?2??+ ?3?? ??as a constraint Solvable by quadratic programming
The quadratic program is: min1 2?????? ????? ?.?.?? ? Solved in MATLAB quadprog(A *A,-A *C,-A,-C) For gcd example, ? = [ 2,1,1] Bound ? ? + ? 2
while while print x print y (1,1) (2,1) x=1, y=3 while assert Data ML
assume(x>0 && y>0); a := x; b := y; c := 0; while( x!=y ) do c := c + 1; if( y > x ) y := y x; if( x > y) x := x-y; assert(c <= a+b-2); od Bound: ? ? + ? 2 Difficult to validate Infer invariants from tests
assume(x>0 && y>0); a := x; b := y; c := 0; while( x!=y ) do print(c, a, b, x, y); c := c + 1; if( y > x ) y := y x; if( x > y) x := x-y; assert(c <= a+b-2); od Predict a bound onc Same tests, more data Solve same QP ?has five columns [1,a,b,x,y] ?hascat every iteration
assume(x>0 && y>0); a:=x; b:=y; c := 0; free_inv(c<=a+b-x-y); while( x!=y ) do c := c + 1; if( y > x ) y := y x; if( x > y) x := x-y; assert(c <= a+b-2 ); od Obtain ? ? + ? ? ? Add as a free invariant Use if checker can prove Otherwise discard
Give program to assertion checker Inductive invariant for gcd example: ? ? + ? ? ? ? > 0 ? > 0 If check fails then return a cex as a new test
u := x;v := y;w := z; while ( x >= y ) do if ( z > 0 ) z := z-1; x := x+z; else y := y+1; od Given degree 2, ? [1,?,?,?,??,??,??,?2,?2,?2] Bound: ? 1.9 + ? ? + 0.95? + 0.24?2 After rounding: ? 2 + ? ? + ? + ?2
Requirements from assertion checker: Handle non-linear arithmetic Consume free invariants Produce tests as counter-examples Micro-benchmarks: Use SGHAN 13 Handles non-linear arithmetic, no counter-examples Windows Device Drivers: Use Yogi (FSE 06) Cannot handle non-linear, produce counter-examples
Regression: Goldsmith et al. 07 , Huang et al. 10, Mining specifications from tests: Dallmeier et al. `12, Termination: Cousot `05, ResAna, Lee et al. 12, Bounds analysis: SPEED, WCET, Gulavani et al. `08, Invariant inference: Daikon, InvGen, Nguyen et al.`12,
Use tests for termination proofs Infer bounds and invariants using QP Use off-the-shelf assertion checkers to validate Future work: disjunctions, non-termination
Partition using predicates a = i ; b = j ; while(i<M || j<N) i = i+1; j = j+1; ? < ? ? ? ? ? ? ? ? ? < ? ? ? ? ? < ? ? < ? ? ? + ? ? ? Control flow refinement Sharma et al. 11
