Supervisor

Suitable for

Abstract

CProver has an interpreter for goto programs but it could be improved, for example adding support for dynamic analysis, calls to external functions and possibly even mixed concrete and symbolic execution. It would also be good to be able to interpret traces found by BMC to catch mismatches / bugs between the logical model and the bit blasting models. This would also be useful for more advanced CEGAR like techniques