gazer icon indicating copy to clipboard operation
gazer copied to clipboard
verified publisher icon ftsrg

Fixes related to Gazer 2.0

Open sallaigy opened this issue 4 years ago • 2 comments

sallaigy avatar Oct 13 '21 17:10 sallaigy

Seems like a lot of work! What are the longer term plans? It would be nice to have Gazer and Theta as part of a portfolio again, even if Theta does not (necesseraly) use Gazer as a frontend. Having a BMC pass first would still be super useful. Do you plan to incorporate other analyses? I think even if CEGAR-based methods do not align well with SSA, k-induction or IC3 could also work well.

hajduakos avatar Oct 26 '21 21:10 hajduakos

Seems like a lot of work! What are the longer term plans? It would be nice to have Gazer and Theta as part of a portfolio again, even if Theta does not (necesseraly) use Gazer as a frontend. Having a BMC pass first would still be super useful. Do you plan to incorporate other analyses? I think even if CEGAR-based methods do not align well with SSA, k-induction or IC3 could also work well.

Indeed, and there are some other things I would like to do. I have two main points in mind:

  1. Releasing a new major version of Gazer, compatible with the new Clang/LLVM versions, and fixing some weird dependency issues.
  2. I am researching some ways to help the BMC algorithm prove correctness better. Currently I am experimenting with abstract interpretation to generate invariants, but it indeed would be interesting to explore k-induction and IC3 as well.

If you have the time, we could have a chat about this sometime :)

sallaigy avatar Oct 27 '21 18:10 sallaigy