search

ftsrg / gazer

An LLVM-based formal verification frontend for C programs.
24 stars 5 forks source link

Fixes related to Gazer 2.0 #99

Open sallaigy opened 2 years ago

hajduakos commented 2 years ago

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.

sallaigy commented 2 years ago

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 :)