Using dynamically generated invariants to help static analyzers to prove properties that they cannot prove previously

[nguyenthanhvuh]

• New Project Idea: Automatic way to help existing Verification tools

  • Ultimate cannot verify a postcond
  • Run DIG to get cand loop invariants
  • Run Ultimate to verify candidate invs
    • Loop: do this until can verify all candidate invs (or find counterexamples to remove them)
    • The reason is that it could be that Ultimate cannot verify some candidate invariants and only can prove them AFTER proving some other candidate ones
  • Assume proved invariants
  • Run Ultimate to prove postcond it cannot prove before

• Benchmarks

  • SV-COMP NLA
  • some other ones ?
  • Multiple verification tools? Seahorn, Ultimate Tapan, Ultimate Anomizer, CPAChecker etc

• Implementation Details

  • Use multiple verifiers to prove properties, run them simultaneously