Abstract

A memoization extension for KLEE. With MoKlee, solver results can be re-used between executions. A sophisticated divergence detection ensures that re-executed paths are valid.

Joint work with Martin Nowack and Cristian Cadar.