[klee-dev] Is running KLEE on arbitrary programs safe?

[Frank Busse]

Hi,


On Fri, 25 Apr 2025 15:46:51 +0000
Burhan Akin Y <burhan_250 at 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