General

Profile

Pavel Shved

Issues

Projects

Activity

08/03/2013

10:58 PM Linux Driver Verification Bug #1312: Timeout script sometimes fails with "No child processes" message
If wait is interrupted by a signal, it will return EINTR rather than ECHILD. In any case, the SIGALRM can arrive bet...
12:29 PM Linux Driver Verification Bug #1312: Timeout script sometimes fails with "No child processes" message
FYI, it was a race condition between waitpid and alarm. If wait4 syscall reaps the child process, but alarm is deliv...

01/02/2013

09:22 AM Linux Driver Verification Bug #3834: SMT sovler answer is strange: Error: Invalid top level command.
Did you follow this piece of instructions from the README file?...

11/07/2012

11:38 AM BLAST Support #3662: Blast documentation?
Vadim Mutilin wrote:
> For *Linux drivers* we use options
> -predH 7 -lattice -include-lattice symb -include-latti...

04/04/2012

11:51 PM BLAST Bug #2705 (Open): BLAST knows something about huge integer numbers?
OCaml doesn't support unsigned 64-bit integers. The maximum value of an integer constant is 2⁶³. See "the documenta...
11:06 PM BLAST Bug #2699: BLAST doesn't find an error in a rather simple example with division
CSIsat interpolating prover doesn't seem to support division. BLAST replaces the division by an uninterpreted funct...
07:52 PM BLAST Bug #2705: BLAST knows something about huge integer numbers?
Did you try using -sv-comp flag?

03/25/2012

07:42 PM BLAST Bug #2264 (Closed): Improve descriptions of legitimate exceptions
Yes, that's pretty much everything I planned for this feature.

02/19/2012

10:40 PM BLAST blast-2.7.1-bin-i686.tgz
Binary distribution of BLAST 2.7.1 for i686
10:37 PM BLAST blast-2.7.1-bin-x86_64.tgz
Binary distribution of BLAST 2.7.1 for x86_64

Also available in: Atom