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.

Publications

• Decision Procedures for Region Logic [pdf] In VMCAI 2012.
  Stan Rosenberg, Anindya Banerjee, David Naumann.
  
• Region Logic: Local Reasoning for Java Programs and its Automation [pdf] (PhD dissertation defended June 2011)
  Stan Rosenberg.
• Local Reasoning for Global Invariants, Part I: Region Logic [pdf] To appear in J.ACM 2013. (This is final version plus index of definitions.)
  Anindya Banerjee, David Naumann, Stan Rosenberg.
  (pdf with additional proofs)
• Local Reasoning for Global Invariants, Part II: Dynamic Boundaries [pdf] To appear in J.ACM 2013. (This is final version plus index of definitions.)
  Anindya Banerjee, David Naumann.
  (pdf with additional proofs)
• Local Reasoning and Dynamic Framing for the Composite Pattern and its Clients. [pdf]
  Stan Rosenberg, Anindya Banerjee, David Naumann. VSTTE 2010.
• Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions [pdf]
  David Naumann, Anindya Banerjee. ESOP 2010.
• Regional Logic for Local Reasoning about Global Invariants. [pdf]
  Anindya Banerjee, David Naumann, Stan Rosenberg. ECOOP 2008.
• Boogie Meets Regions: a Verification Experience Report [pdf]
  Anindya Banerjee, Mike Barnett, David Naumann. VSTTE 2008.

Downloads

• VERL 1.1+examples (8 Mb)
(Unzip and run setup.exe; see readme.txt, release_notes.txt in the distribution sub-directory.)
• Automated Test Harness for VERL 1.1 (Optional)
(Unzip and see readme.txt)

^* 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.