A First-Order Logic with Frames

Adithya Murali, Lucas Peña, Christof Löding, P. Madhusudan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We propose a novel logic, called Frame Logic (FL), that extends first-order logic (with recursive definitions) using a construct that captures the implicit supports of formulas— the precise subset of the universe upon which their meaning depends. Using such supports, we formulate proof rules that facilitate frame reasoning elegantly when the underlying model undergoes change. We show that the logic is expressive by capturing several data-structures and also exhibit a translation from a precise fragment of separation logic to frame logic. Finally, we design a program logic based on frame logic for reasoning with programs that dynamically update heaps that facilitates local specifications and frame reasoning. This program logic consists of both localized proof rules as well as rules that derive the weakest tightest preconditions in FL.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems- 29th European Symposium on Programming, ESOP 2020 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings
EditorsPeter Müller
PublisherSpringer
Pages515-543
Number of pages29
ISBN (Print)9783030449131
DOIs
StatePublished - 2020
Event29th European Symposium on Programming, ESOP 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 - Dublin, Ireland
Duration: Apr 25 2020Apr 30 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12075 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference29th European Symposium on Programming, ESOP 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020
CountryIreland
CityDublin
Period4/25/204/30/20

Keywords

  • First-Order Logic
  • First-Order Logic with Recursive Definitions
  • Heap Verification
  • Program Logics
  • Program Verification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A First-Order Logic with Frames'. Together they form a unique fingerprint.

Cite this