CSolve
Liquid Types-Based C Program Verifier

CSolve is a Liquid Types-based verifier for C programs which can verify sophisticated program properties like memory safety, deterministic parallel execution, and invariants of linked data structures, while imposing an extremely low annotation overhead on the programmer.

Demo

Try the CSolve online demo.

Source Code

The latest release of CSolve: csolve-2012-04-24.tar.gz.

Publications

CSolve is based on Low-Level Liquid Types, a refinement type system for low-level languages which supports type inference using the Liquid Types technique.

CSolve

Low-Level Liquid Types

Liquid Types

Personnel