General

Profile

Sepideh Asadi

Issues

Projects

Activity

28/11/2018

22:43 hifrog To do #9433 (New): strong itp-lra-algorithm generates redundant formula
investigate LRA strong itp Alg and compare the result with weak one; it seems weak mode generates compact and good su...

08/09/2018

20:23 hifrog To do #7864 (New): investigate the functionality of --no-assert-grouping
2-Enable this functionality:
--no-assert-grouping : do not group checks for the same assertion with the dif...
20:19 hifrog To do #7863 (New): report system in HiFrog
Design a separate class as a report class in HiFrog (storing in the Buffer beforehand) - (due to performance)
20:08 hifrog To do #7862 (New): enable summary re-use in CUF
CUF generates summary but does not reload(re-use) it.

07/09/2018

22:19 hifrog To do #7861 (New): A minimal necessary unwinding bound
A minimal necessary unwinding bound
A lazy enumeration of unrollings, it is something that CBMC is doing in SVCOMP.
22:15 hifrog To do #7860 (New): follow up in EUF summaries (Grisha's idea)
The point is about the loop in function func which calculates a new value for variable b. This loop is not needed for...
22:01 hifrog To do #7859 (New): checks for uninitialized locals in CBMC
CBMC in the goto-instrument program supports --uninitialized-check.
Since we updated cprover to version 5.10, it is ...

29/08/2018

13:04 hifrog Bug #7805 (New): UFInterpolator.C
*File*: sumth60.c (attached)
*How to run:*
--logic qfuf --claim 2
*Error message:*
RESULT: UNSAT - it holds!...

07/08/2018

18:49 hi-bench Revision 7025a1ac: added SVCOMP 2018 verification tasks
18:44 hi-bench Revision 6ea68f2b: delete some benchmarks

Also available in: Atom