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.

Stan Rosenberg designed and implemented the system as part of his PhD dissertation supervised by Anindya Banerjee and Dave Naumann.



Distribution for a Windows platform:

* This material is based upon work supported by the US National Science Foundation under Grants supported by US NSF awards CNS-0627338, CRI-0708330 and CCF-0915611 (to Stevens Institute of Technology) and CNS-0627748 (to Kansas State University).
Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.