Added by Roopak Sinha over 11 years ago. Updated over 11 years ago.
0%
Description
Hi,
How different are the new Blast versions from 2.5? I find the newer versions to be much better (performance wise), but cannot find documentation/manuals on the new site.
Please advise.
Regards,
Roopak
Files
| Simplest.c (1.35 KB) Simplest.c | Roopak Sinha, 11/07/2012 01:54 AM |
Top level description of changes is available at the News page:
http://forge.ispras.ru/projects/blast/news
More detailed description was published at TACAS'12:
http://sv-comp.sosy-lab.org/2012/submissions/tacas2012_submission_199_BLAST%202.7.pdf
The description of options is available with
pblast.opt --help
Supported options are above the section:
Old Heuristics that are no longer used/supported
For Linux drivers we use options
-predH 7 -lattice -include-lattice symb -include-lattice list -craig 2
-stop-sep -merge bdd
Also
-main for entry point
-L for error label
If you want alias analysis, then add:
-alias bdd
-cref
-nomusts -const
Option used for SV-COMP'12 are described in the section:
Software Verificaiton competition 2011 options
Thanks, that's great.
I have a simple program that seems to be taking forever for Blast to verify (it should be safe IMHO). The program in question is attached (I am looking for the possibility of reaching the ERROR label).
Is there any way to make Blast converge faster, or perform bounded verification?
Also, should I have opened a new request for this question?
Thanks,
Roopak
Vadim Mutilin wrote:
For Linux drivers we use options
-predH 7 -lattice -include-lattice symb -include-lattice list -craig 2
-stop-sep -merge bdd
So, this is precisely the reason why we should document BLAST more. :) -predH 7, -craig 2, -stop-sep and -merge bdd are default, and there's no need to specify them in latest versions of blast.
If you want alias analysis, then add:
-alias bdd
-cref
-nomusts -const
It should be simplified to one single -analyze-aliases option. :( Verifiers should "just work".
As per Simple.c program, after 20 minutes of verification the underlying solver consumed all my memory, and the verification didn't complete. It feels like it should complete sooner or later if the underlying tools are good enough.