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...
Patrick Maxim Rondon, Alexander Bakst, Ming Kawagu...
We present Low-Level Liquid Types, a refinement type system for C based on Liquid Types. Low-Level Liquid Types combine refinement types with three key elements to automate verifi...
Ming Kawaguchi, Patrick Maxim Rondon, Ranjit Jhala