gazer
gazer copied to clipboard
ftsrg
An LLVM-based formal verification frontend for C programs.
Dear Developer. I noticed your tool by reading the paper "Gazer-Theta: LLVM-based Verier Portfolio with BMC/CEGAR (Competition Contribution)" and I found that the LLVM IR is converted into a CFA....
Resolves #96. Note that this would mean that only LLVM11 works, changes are still needed for this to work on both versions. (I don't know about LLVM10 or 8 or...
This commit adds a fix for a few typos in the portfolio (which caused the output to be wrong in certain cases) and a two additional portfolio configuration YAMLs.
This PR contains the first patch aiming to allow usage of LLVM tools (mostly `opt`) in the project. Usage of `opt` would enable single pass tests, or later, even remove...
Someone mentioned that we could upgrade LLVM framework (current version is 9). There are many different aspects to this, so I think it is useful to start a discussion to...
This is the first patch aiming to enable generating Theta-XCFA. This PR refactors the monolith that is ThetaCfaGenerator.
Previously Theta could only parse 32-bit integer literals, but with 1.7 (see #29) it should not be a limitation. We should check if Gazer has to be modified internally to...
I'll need to take a look at exactly what the problem is here. It could be a performance issue, but it probably can be handled so that this issue is...
I don't know if it actually works or not, we should try first.