[klee-dev] pathcondition for concrete values
c.cadar at imperial.ac.uk
Wed Jun 29 03:36:10 PDT 2011
Hi Leandro, Vijay,
We are currently experimenting with starting execution from a set of
concrete inputs; we can share our results and changes once we are done.
There is actually already some support for this in the open-source
version of KLEE: just grep the help options for the "seed" functionality.
On 29/06/11 08:10, Leandro Sales wrote:
> 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>
>>> Is there a way to use klee to extract the path condition followed for a
>>> given input (or file)?
>>> klee-dev mailing list
>>> klee-dev at keeda.stanford.edu
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
More information about the klee-dev