Mark Gritter (markgritter) wrote,
Mark Gritter

Klee -- symbolic execution of real programs

Klee is a project which symbolically executes computer programs, looking for crash conditions or other errors. It can be used to automatically generate test cases with a very high degree of coverage.

The basic idea is to make variables hold symbolic expressions instead of concrete ones. So executing a statement like "a=b*c" doesn't actually execute multiplication, it just notes that now "a" holds the value "Multiply(b,c)". When you get to a point where there's a test on the value of "a", you run a constraint checker (an automated prover) to decide if the test could be true or not, and if true with what set of variables. So you could find, for example, an integer overrun by checking whether "a" is always positive; and if not it'll give you values of "b" and "c" that demonstrate it's not. (Or, more likely, the values of the inputs that led to "b" and "c" having the values which led to integer overflow.)

This seems like a very strong tool for systems programming. I've been thinking of playing around with the idea of a language whose compiler produces correctness proofs along with generated code. But this will work on (most) C code--- they ran it on the GNU Coreutils collection. The project seems to be reasonably active (the original paper was 2008).
Tags: programming, software
  • Post a new comment


    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 1 comment