[klee-dev] pathcondition for concrete values
leandro.shp at gmail.com
Wed Jun 29 00:10:15 PDT 2011
Thanks Vijay. For your better explanation of my question.
@David, my problem is a little more complex then just saying Klee to write
path-constraints. Maybe I was not completely clear in my question. I want to
go in the "reverse" way that Klee usually goes. Instead of executing my
program symbolically, extract path constraints (.pc) and get a solution
(.ktest), I want to find the path constraints based on a ktest file (that
represents my input), that I have already generated.
Is that possible?
On Wed, Jun 29, 2011 at 4:45 AM, Vijay Ganesh <hellovijay at gmail.com> wrote:
> Generalizing on Leonardo's question:
> Have there been extensive experiments using KLEE in the whitebox
> fuzzing mode (similar to SAGE), i.e., using a seed set of inputs to
> extract paths, and then solving them (typically offline) to explore
> branches on these paths? The goal here is to look for deep errors, as
> opposed to the typical usage-scenario of coverage.
> Vijay Ganesh.
> On Tue, Jun 28, 2011 at 3:21 PM, Leandro Sales <leandro.shp at gmail.com>
> > Hi,
> > Is there a way to use klee to extract the path condition followed for a
> > given input (or file)?
> > thanks,
> > Leandro
> > _______________________________________________
> > klee-dev mailing list
> > klee-dev at keeda.stanford.edu
> > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the klee-dev