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.