[klee-dev] Klee path statistics and merging options

[Carril Rodriguez, Luis Manuel (IPD)]

Hi,

   about the slicing this work could interest you:

http://www.fi.muni.cz/~xstrejc/publications/tacas2013preprint.pdf


   Basically they have a llvm pass that perform the program slicing before running it under KLEE, reducing effectively the search space.


Cheers

Luis M.


________________________________
From: klee-dev-bounces at imperial.ac.uk <klee-dev-bounces at imperial.ac.uk> on behalf of RAJDEEP MUKHERJEE <rajdeep.mukherjee87 at gmail.com>
Sent: 17 December 2015 03:08
To: klee-dev at imperial.ac.uk
Subject: [klee-dev] Klee path statistics and merging options



Hi,

I have the following queries regarding Klee. I would really appreciate any help.

1> How to obtain the following statistics from Klee:
  A> Total number of feasible paths,
  B> Total number of infeasible paths,
  C> Total number of paths in the program.
  D> Total number of solver queries and
  E> Total time spent in solver

2> Does Klee perform any state merging or path-merging ? What option to use for this ?

3> Does Klee perform property driven slicing before it begins symbolic execution ?

Many thanks in advance.

Best,
Rajdeep

--



-------------- next part --------------
HTML attachment scrubbed and removed