"KLEE-PROVER"
Supervisor
Suitable for
Abstract
Alter the CBMC symbolic execution engine to create a dynamic symbolic execution tool similar to KLEE. Possible features include:
• Distributed and incremental support using the caching scheme here
• A feature to run BMC as you go to explore the traces 'around' the execution traces
• Use path exploration as the witness generation part of an ACDL process.
• Perform precondition inference, possibly using ACDL.