[klee-dev] Test framweork for Haskell that leverages Klee

[Paul Marinescu]

Hi Mario,
This is a really interesting project. I’m wondering about two things:
1. How do you introduce symbolic data? Does the Haskell program need to be manually instrumented with klee_make_symbolic calls? grep-ing through your repo, I didn’t find any --sym-arg(s) or klee_make_symbolic
2. How do you make KLEE behave concolically? While the terminology is not standardised, I think there’s some agreement that KLEE itself is not a concolic execution tool (despite what Wikipedia might suggest).

Paul

> On 15 Jun 2015, at 02:04, Mario Alvarez Picallo <mario.alvarez739 at gmail.com> wrote:
> 
> Hello all,
> 
> As a part of my Master's Thesis, I'm currently working on scher, a prototype concolic testing framework for Haskell code that uses Klee under the hood.
> 
> It uses the JHC haskell compiler, that compiles Haskell to surprisingly small C programs that are then compiled to LLVM via llvm-gcc to be analyzed by Klee.
> 
> Feel free to take a look at the current work, that you can find here <https://github.com/m-alvarez/scher>, and tell me what you think, ask questions, make requests or point out bugs (either via github's integrated issue tracker or via mail).
> 
> Cheers!
> 
> -- 
> Now I do not know whether I was then a lambda expression emulating a Turing machine, or whether I am a Turing machine emulating a lambda expression.
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
HTML attachment scrubbed and removed