Formal Methods @ UCF
Yuyan Bao
|
I am a Ph.D student working in the Formal Methods Lab at University of Central Florida. My research interests include specification andverification language, programming analysis and programming tools. View My Website |
|
Research Projects
My research is about investigating different methodologies of specifying frame properties, including the universe type system, dynamic frames, implicit dynamic frames, region logic and separation logic.
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.