[klee-dev] About KLEE, how to extract path conditions

[Meixian Chen]

To the attention of the KLEE staff,

Thanks for your reply. We are trying to analysis the constraint queries
reusing opportunities in a single program and across different programs. We
try to collect constraint by KLEE after optimisation like simplification
and independence, but not cache. How could we achieve that?

Best regards,
Meixian Chen, Andrea Aquino




On Wed, Feb 19, 2014 at 10:43 AM, Andrea Aquino <andrex.aquino at gmail.com>wrote:

> To the attention of the KLEE staff,
>
> first of all we would like to introduce ourselves.
> My name is Andrea Aquino while my colleague's name is Meixian Chen, we are
> Ph.D. students at Università della Svizzera Italiana (Switzerland, Ticino).
>
> We are currently looking for a way to extract path conditions produced by
> KLEE. Actually we will need to save on disk the symbolic constraints
> produced by KLEE during its execution in a human readable format.
>
> For example if analysing a program KLEE calculates 3 path conditions:
> 1. x > 0
> 2. y > 0 && y < 5
> 3. x + y < 10
>
> we would like to store them in a file in order to perform a posteriori
> checks on them.
> We don't care about redundancy (the same constraint stored two or more
> times).
>
> Is there an easy way to achieve this goal?
> How can we proceed?
>
> Best regards,
> Andrea Aquino, Meixian Chen
-------------- next part --------------
HTML attachment scrubbed and removed