[klee-dev] Inquiry About Compositional Symbolic Execution and Function Summary Generation in KLEE

[刘乔森]

Dear KLEE Development Team,

I hope this email finds you well. I am currently exploring tools for compositional symbolic execution and am particularly interested in KLEE’s capabilities in this area. My research involves generating function summaries to enhance the scalability of symbolic execution for large programs.

I understand that KLEE is a powerful dynamic symbolic execution engine built on the LLVM infrastructure, widely used for test case generation and bug finding. However, I am unsure whether KLEE officially supports compositional symbolic execution, specifically the generation of function summaries (e.g., capturing preconditions and postconditions for function paths).

Could you please clarify if KLEE has built-in support for generating function summaries as part of compositional symbolic execution? If so, could you provide guidance on how to enable or implement this feature? Alternatively, if this functionality is not natively supported, are there any recommended extensions, forks, or related tools (e.g., MACKE) that integrate compositional analysis with KLEE?

Thank you for your time and assistance. I greatly appreciate any insights or pointers to relevant documentation or resources.

Best regards,
Lqs66
-------------- next part --------------
HTML attachment scrubbed and removed