Zvonimir Rakamaric
Zvonimir Rakamaric
It would be good to write a short tutorial describing this.
It would be good for SMACK to actually generate precise modifies clauses, instead of relying on a back-end verifier to support inference of modified globals. The way I see it,...
There are indications that unused axioms and declarations sometimes slow down verification. On top of that, they make our generated Boogie files daunting to read, especially for novice users. I...
Currently it seems that it is impossible to invoke Boogie in modular verification mode (i.e., no unrolling) from the SMACK script. It is unclear what the best solution to this...
So SMACK fails to find a bug in this benchmark, despite reaching a large number of unrolls. I checked the results form last year, and none of the verifiers returned...
If I am reading this right, the AWS category has no false benchmarks. This doesn't seem like a good idea since it can really skew the results - for example...
See this line for example: https://github.com/sosy-lab/sv-benchmarks/blob/4c95243e3aff4b6c8da7a8c6ce18feb2a8306738/c/floats-cbmc-regression/float-rounding1_true-unreach-call.i#L1092 According to the specification for these functions: "Attempts to establish the floating-point rounding direction equal to the argument round, which is expected to be...
Here is the current model: ``` int munmap(void *addr, size_t length) { if(__VERIFIER_nondet_int()) return -1; (void)length; free(addr); return 0; } ``` It might nondeterministally not free memory, which causes memory...
Several people asked me about this, given the recent trend in ML (and other areas) to use low, custom bit-widths for floating-points. I suspect this would not be that hard...
@Thanhson89, who is a PhD student at Utah, has been investing a lot of time to understand the source code of FPTaylor. He is documenting his findings along the way,...