Static verification made easy by fractional ownership!
Check
About ConSORT - Static assertion checker for heap-manipulating programs
ConSORT is a static assertion cheker for a simple imperative language for heap-manipulating programs. The underlying theory is based on the combination of fractional ownership and refinement types.
Project Home