We present CSolve, an automated verifier for C programs based on Liquid Type inference. We show how CSolve verifiess memory safety through an example and describe its architecture and interface.
Proceedings of the 24th International Conference on Computer-Aided Verification (CAV 2012).