Verifier for Region Logic (VERL): VERL translates a program specified in region logic to a Boogie 2 program. VERL is a descendant of Dafny. While retaining most of the features of Dafny’s programming language, VERL’s specification language is aimed at region logic. Its key features include the full generality of region assertions and effects, localized framing (code blocks annotated with assertions whose truth must be preserved), and derivation of read effects of assertions.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element