CSolve: Verifying C with Liquid Types

摘要

We present CSOLVE, an automated verifier for C programs based on Liquid Type inference. We show how CSOLVE verifies memory safety through an example and describe its architecture and interface.