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
References in zbMATH (referenced in 2 articles )
Showing results 1 to 2 of 2.
- Banerjee, Anindya; Naumann, David A.; Rosenberg, Stan: Local reasoning for global invariants. I: Region logic (2013)
- Rosenberg, Stan; Banerjee, Anindya; Naumann, David A.: Decision procedures for region logic (2012)