Siddharth Krishna - NYU Computer Science

1 Siddharth Krishnaprocedureinsert(lst: Node, elt: Node) returns(res: Node)requires , ensures ( , ){if(lst!= null){varcurr:= lst;while(nondet() && != null)invariant , , {curr:= ;} := ; := elt;returnlst;}elsereturnelt;}procedurei nsertion_sort(lst: Node) requires , ensures ( , ){varprv:= null, srt:= lst;while(srt!= null)invariant( = = ( , ))||( ( , ) ( , )){varcurr:= ;varmin := srt;while(curr!= null) invariant = , , , , ||( ( , ) ( , ) , , ( , ))invariant {if( < ) {min := curr;}curr:= ;}vartmp:= ; := ; := tmp;prv:= srt;srt:= ;}}procedureinsert(lst: Node, elt: Node) returns(res: Node)requires , ensures ( , ){if(lst!)}

2 = null){varcurr:= lst;while(nondet() && != null){invariant ( , ) , curr:= ;} := ; := elt;returnlst;}elsereturnelt;}.. ( , ) , x1 x1 x1 x1 x1 =1 , . = ( , )k1 , . , .. ( )Formulas ( , ) , Graphs | | | | 2 3456.

3 | | ls , ,..| tree ,.. 0 , , , , .. , , .. ls , ,_| tree ,_ , , | 2 3456 | 2 3456 2 3456 2 3456 Numeric Invariants: Training at verification time Training data: Observations Desired Invariant~ ModelOur Heap Invariants: Training beforehand Training data: Independent Desired Invariant ~ Predicted slides from David Sontag, adapted from Luke Zettlemoyer, VibhavGogate, Carlos Guestrin, Andrew Moore, Dan Kleinprocedureinsert(lst: Node, elt: Node) returns(res.)

4 Node)requires , ensures ( , ){if(lst != null){var curr := lst;while( ? && != null){curr := ; } := ; := elt;returnlst;}} ( , ) , procedureinsert(lst: Node, elt: Node) returns(res: Node)requires , ensures ( , ){if(lst != null){var curr := lst;while( ? && != null)invariant ( , ) , {curr := ; } := ; := elt;returnlst;}}Grasshopper picture from this bloglseg(lst, curr)[][2][2, 4]lseg(curr, null)[2, 4, 6, 9][4, 6, 9][6, 9]lseg(elt,null)[7][7][7] . , . < . , . , : + .. , . , : + .. Analog to functional version from:He Zhu, Gustavo Petri, Suresh Jagannathan, Automatically Learning Shape Specifications, PLDI 2016 Picture from Aqua Teen Hunger Force Wikia