How could you adapt KLEE to check for bugs in JOS (e.g., what sorts of symbolic inputs could you use and what could you test)? Could you use KLEE to find some of the bugs you've encountered during the term? Feel free to recount mind-numbing debugging marathons here. :)