Project Description

DafnyR is an experimental tool for sequential program specification and verification. It is a variant of Dafny and is inspired by region logic. DafnyR preserves most of the features of Dafny Language. DafnyR is built on a fine-grained region logic and allows one to use several styles of specification frame properties in sequential programs: dynamic frames, region logic and separation logic.

Yuyan Bao extends Dafny to DafnyR as part of her Ph.D work supervised by Gary T. Leavens.


Last edited Mar 11, 2013 at 3:24 PM by Yuyan, version 7