AUTOMATIC
VERIFICATION OF
LOOP INVARIANTS
Olivier Ponsini, Hélène Collavizza, Carine F...
Outline
2/8
 Loop invariants are useful
 Automatic generation may produce spurious loop
invariants...
Why loop invariants?
3/8
Program testing and
verificatio...
How to obtain loop invariants?
4/8
Correct
Automatic generation ...
Verification of loop invariants
5/8
{I  Cond} Body {I}
Hoare rule:
...
CPBPV
6/8
 Constraint-based program verification
 JML (Java Modeling Language) pre and post conditions...
Experimentations
7/8
 5 classical programs from # checked invariants (32 bits)
verification domain 160 ...
Conclusion and perspectives
8/8
 An effective checker for candidate loop invariants
 Refuting spurious...
of 8

Ponsini automatic slides

Published on: Mar 4, 2016
Source: www.slideshare.net


Transcripts - Ponsini automatic slides

  • 1. AUTOMATIC VERIFICATION OF LOOP INVARIANTS Olivier Ponsini, Hélène Collavizza, Carine Fédèle, ICSM 2010 Claude Michel, Michel Rueher
  • 2. Outline 2/8  Loop invariants are useful  Automatic generation may produce spurious loop invariants We contribute a constraint-based approach for effectively filtering out spurious invariants
  • 3. Why loop invariants? 3/8 Program testing and verification Program design and implementation Program maintenance • Program understanding and documentation • Error finding and correction • Optimization and refactoring
  • 4. How to obtain loop invariants? 4/8 Correct Automatic generation Interproc Time demanding of correct invariants InvGen Weak invariants Fast Automatic generation Daikon Strong invariants of candidate invariants Gin-Pink Spurious Fast Candidate Invariant Strong invariants checking Correct
  • 5. Verification of loop invariants 5/8 {I  Cond} Body {I} Hoare rule: {I} while (Cond) Body {I  Cond} /*@ requires Pre  Base case: @ ensures Post @*/ ... method(...) { Pre  enc(Init)  I Init while (Cond) {  Inductive case: Body } I  Cond  enc(Body)  I Final }
  • 6. CPBPV 6/8  Constraint-based program verification  JML (Java Modeling Language) pre and post conditions  On-the-fly execution path exploration  Refutation proof with counter-example JML annotated methods  Bounded approach method2 method3  Integer domain size method1  Array size False assertions + test cases CPLEX CP  True CPBPV assertions
  • 7. Experimentations 7/8  5 classical programs from # checked invariants (32 bits) verification domain 160 Time out 140 < 1min 120  180 candidate invariants 100 from different sources 80  Heuristics (125) <1s 60  Daikon (48) 40  InvGen (3) 20 Time out < 1min  Textbooks (7) 0 <1s Valid Spurious  8, 16, and 32-bit integers
  • 8. Conclusion and perspectives 8/8  An effective checker for candidate loop invariants  Refuting spurious invariants is fast  No false positive  Test cases are produced as counter-examples  Perspectives  Extend to programs with multiple and nested loops  Integrate CPBPV

Related Documents