[klee-dev] Target-Directed Symbolic Execution with KLEE

[Cristian Cadar]

Hi Yannic, you might like to take a look at KATCH: 
http://srg.doc.ic.ac.uk/projects/katch/

The code is available, but unfortunately not integrated into the mainline.

Cristian

On 23/01/17 15:31, Yannic Noller wrote:
> Hi Jason,
>
> thanks, I know the example and you are right: this is probably the
> fastest way to try my idea. But this means that there is no special
> option for an target-oriented search, right? For example I do not want
> to follow paths that cannot reach my specified target line in order to
> cut down the possible state space. If not, is it easy to implement such
> a feature in KLEE?
>
> Thanks!
> — Yannic
>
>
>> On 23 Jan 2017, at 14:12, Papapanagiotakis-Bousy, Iason
>> <iason.papapanagiotakis-bousy.15 at ucl.ac.uk
>> <mailto:iason.papapanagiotakis-bousy.15 at ucl.ac.uk>> wrote:
>>
>> Hi Yannic,
>>
>> Have you looked into the maze
>> tutorial https://feliam.wordpress.com/2010/10/07/the-symbolic-maze/ ?
>>
>> I am no KLEE veteran but here is my suggestion:
>> If I understand correctly what you are trying to achieve, then you
>> could use what is shown in the tutorial and at the end instead of
>> looking at the .ktest files that will have concrete examples, read the
>> corresponding .kquery files that contain the path constraints.
>>
>> (because the tutorial uses an older version of KLEE, constraints are
>> stored in a .pc instead of .kquery)
>>
>> Hope it helps.
>>
>> Best regards,
>> Jason
>>
>> *From:* klee-dev-bounces at imperial.ac.uk
>> <mailto:klee-dev-bounces at imperial.ac.uk>
>> [mailto:klee-dev-bounces at imperial.ac.uk] *On Behalf Of *Yannic Noller
>> *Sent:* Monday, January 23, 2017 2:54 PM
>> *To:* klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
>> *Subject:* [klee-dev] Target-Directed Symbolic Execution with KLEE
>>
>> Hi all,
>>
>> I would like to create all path conditions (or an under-approximation)
>> that reach a certain source code line (something like "directed
>> symbolic execution"). Is there an option in KLEE to do that? Or is
>> there an extension of KLEE that can do that?
>>
>> Any help is very appreciated :)
>>
>> Thanks,
>> Yannic
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>