AISE is a static verifier that combines abstract interpretation and symbolic execution techniques. The verification approach is based on a verification framework that combines abstract interpretation and symbolic execution in a novel way.
AISE is implemented based on Clam and KLEE. AISE also calls ESBMC when it detects programs containing floating-point data (less than 50 programs have floating-point data in the ReachSafety-Loops category), because AISE is unable to handle floating-point data. (AISE doesn't link against ESBMC, it only calls it in special cases.).
/bin/aise <data_model> <input C file>
e.g. ./bin/aise --32 ./bin/array-1.c
./bin/aise --version
It's the first time we try to particapate in SV-COMP, we only focus on a single category "Reachability-Loops". AISE ranked 5th in this category, the results can be found here: (https://sv-comp.sosy-lab.org/2024/results/results-verified/). AISE's archive is publicly avaliable in https://doi.org/10.5281/zenodo.10201159. For more information about the AISE, you can refer to the publication
This year, we still focus on the category "Reachability-Loops". AISE's archive is now publicly avaliable in https://doi.org/10.5281/zenodo.14183670.