Hi,
On Fri, 25 Apr 2025 15:46:51 +0000 Burhan Akin Y <burhan_...@live.de> wrote: > From my understanding of the original paper, KLEE does static code > analysis and uses a theorem prover in the backend. Does KLEE do > anything else beyond making variables symbolic, exploring paths and > solving constraints? KLEE does dynamic analysis and works roughly like an interpreter for LLVM bitcode. That means, when your program under test does funny things KLEE will do funny things. Kind regards, Frank _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev