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... Pavel Shved
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... Pavel Shved

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?... Pavel Shved

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...
Pavel Shved

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... Pavel Shved
07:52 PM BLAST Bug #2705: BLAST knows something about huge integer numbers?
Did you try using -sv-comp flag? Pavel Shved
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... Pavel Shved

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. Pavel Shved

02/19/2012

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

Also available in: Atom