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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
