Relational logic with framing and hypotheses

Anindya Banerjee, David A. Naumann, Mohammad Nikouei

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

20 Scopus citations

Abstract

Relational properties arise in many settings: relating two versions of a program that use different data representations, noninterference properties for security, etc. The main ingredient of relational verification, relating aligned pairs of intermediate steps, has been used in numerous guises, but existing relational program logics are narrow in scope. This paper introduces a logic based on novel syntax that weaves together product programs to express alignment of control flow points at which relational formulas are asserted. Correctness judgments feature hypotheses with relational specifications, discharged by a rule for the linking of procedure implementations. The logic supports reasoning about program-pairs containing both similar and dissimilar control and data structures. Reasoning about dynamically allocated objects is supported by a frame rule based on frame conditions amenable to SMT provers. We prove soundness and sketch how the logic can be used for data abstraction, loop optimizations, and secure information flow.

Original languageEnglish
Title of host publication36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016
EditorsAkash Lal, S. Akshay, Saket Saurabh, Sandeep Sen, Saket Saurabh
Pages11.1-11.16
ISBN (Electronic)9783959770279
DOIs
StatePublished - 1 Dec 2016
Event36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016 - Chennai, India
Duration: 13 Dec 201615 Dec 2016

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume65
ISSN (Print)1868-8969

Conference

Conference36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016
Country/TerritoryIndia
CityChennai
Period13/12/1615/12/16

Keywords

  • Frame conditions
  • Product programs
  • Program equivalence
  • Region logic
  • Relational Hoare logic

Fingerprint

Dive into the research topics of 'Relational logic with framing and hypotheses'. Together they form a unique fingerprint.

Cite this