Conditional Effects In Fine-Grained Region Logic

Keywords

Formal specification; Formal verification; Framing; Hoare logic; Region logic

Abstract

Specification languages have long featured ways to describe what does not change when an imperative procedure is executed: the so-called frame problem. Solutions to the frame problem are needed for formal verification in imperative programming, as otherwise a verification would not be able to accumulate information from one statement to the next. Region logic is one of the approaches to solving the frame problem. We present a modified version of region logic with fine granularity and introduce conditional effects that allows one to specify more precise frame conditions.

Publication Date

7-7-2015

Publication Title

Proceedings for the 17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015: co-located with ECOOP 2015

Document Type

Article; Proceedings Paper

Personal Identifier

scopus

DOI Link

https://doi.org/10.1145/2786536.2786537

Socpus ID

84958745246 (Scopus)

Source API URL

https://api.elsevier.com/content/abstract/scopus_id/84958745246

This document is currently not available here.

Share

COinS