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

[Yannic Noller]

Hi Cristian,

thanks for the hint, I will take a look.

— Yannic

> On 25 Jan 2017, at 16:01, Cristian Cadar <c.cadar at imperial.ac.uk> wrote:
> 
> Hi Yannic, you might like to take a look at KATCH: http://srg.doc.ic.ac.uk/projects/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 <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/ <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 <mailto: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> <mailto: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 <mailto:klee-dev at imperial.ac.uk>
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
-------------- next part --------------
HTML attachment scrubbed and removed