CAUTION: This message came from outside Imperial. Do not click links or open attachments unless you recognise the sender and were expecting this email.
>From my understanding, KLEE provides an abstraction layer to represent >symbolic expressions, i.e., using `klee::Expr`. This abstraction allows KLEE to support multiple solvers rather than a single one, e.g., STP or Z3. This technique should be the one proposed in the paper you mentioned. However, there is only one solver instantiated during the execution, see `std::unique_ptr<TimingSolver>` in https://github.com/klee/klee/blob/master/lib/Core/Executor.h#L112. If you want to run multiple solvers in parallel, you may need to hack `klee::Executor`. Yuzhou On Mon, Mar 16, 2026 at 2:59 PM Yuxiang Lin <[email protected]<mailto:[email protected]>> wrote: CAUTION: This message came from outside Imperial. Do not click links or open attachments unless you recognise the sender and were expecting this email. Dear KLEE Community, I would like to ask whether there is any current work on implementing CAUTION: This message came from outside Imperial. Do not click links or open attachments unless you recognise the sender and were expecting this email. Dear KLEE Community, I would like to ask whether there is any current work on implementing portfolio solving for KLEE at the granularity of each individual solver query or a group of queries. For example, within a single execution, when a branch is encountered, fork() might be called, which in turn makes a solver query. This solver query can then be sent to, for example, both STP and Z3, and fork() can proceed whenever STP or Z3 returns first. For existing work on portfolio solving, I only found KLEE-MultiSolver (https://srg.doc.ic.ac.uk/projects/klee-multisolver/<https://urldefense.com/v3/__https://srg.doc.ic.ac.uk/projects/klee-multisolver/__;!!LIr3w8kk_Xxm!rQUE0mDoObSCZOtpAUqGnr0LVVQR2rGtUi2ZbA2w-OlfJLZ81YOyg2-4XISsuEFXdsW02mg1QVyyq8hW8AaCzqwwdLaJHU10vlE$>), which implemented the metaSMT backend and is already part of KLEE now. However, you can only still use just one solver for one KLEE run. The idea of implementing portfolio solving for individual queries is also discussed in Section 5 of the KLEE-Multisolver report, but I was unable to find any follow-up works. The reason I want to ask this is that for the specific project I ran KLEE on, I have encountered solver timeouts even with very long solver timeout settings (e.g. 5 minutes). I have not done a deep investigation on the offending queries yet, but I just thought that portfolio solving might mitigate this problem to some extent. Best regards, Yuxiang Lin _______________________________________________ klee-dev mailing list -- [email protected]<mailto:[email protected]> To unsubscribe send an email to [email protected]<mailto:[email protected]>
_______________________________________________ klee-dev mailing list -- [email protected] To unsubscribe send an email to [email protected]
