A formal verification framework for static analysis - As well as its instantiation to the resource analyzer COSTA and formal verification tool KeY.