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.

• Type: Journal
• Year: 2012
• Where: CAV
• Authors: Patrick Maxim Rondon, Alexander Bakst, Ming Kawaguchi, Ranjit Jhala
• Keywords: CAV 2012, Hardware, Liquid Type, Memory Safety, Type Inference