The Z3 Theorem Prover released under MIT license

Re:The Z3 Theorem Prover released under MIT license by TheLoneWolfling on Thursday March 26, 2015 @07:58PM (#9273961)

I wonder if that could be implemented as an extension to AFL.

I.e. mutate random values for a while, then use an SMT solver to try to find any remaining code paths that haven't been followed by AFL.

I have a feeling AFL would be faster for "simple" paths, but an SMT solver may be handy for getting those last few paths.

[ Parent | on HN ]

Re:The Z3 Theorem Prover released under MIT license by ulber on Friday March 27, 2015 @01:55AM (#9274936)

My experience with concolic testing has been that single path satisfiability queries tend to be quite cheap and it's actually a bit challenging to write the tooling around the solver in such a way that the solver would actually become the bottleneck. This is not to say that combinations of concolic testing with other testing methods is not an interesting research topic :)

[ Parent | on HN ]

Re:The Z3 Theorem Prover released under MIT license by rurban on Saturday March 28, 2015 @01:07PM (#9282029)

Then rather use cmbc, which does exactly that. It translates C code into SMT rules, allows assertions on symbolic variables and solves them. And note that for harder crypto problems Z3 is not the best, it's just the easiest to use.

[ Parent | on HN ]