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/), 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] To unsubscribe send an email to [email protected]
