TY - GEN
T1 - A First-Order Logic with Frames
AU - Murali, Adithya
AU - Peña, Lucas
AU - Löding, Christof
AU - Madhusudan, P.
N1 - Funding Information:
Acknowledgements: We thank ESOP’20 reviewers for their comments that helped improve this paper. This work is based upon research supported by the National Science Foundation under Grant NSF CCF 1527395.
Publisher Copyright:
© 2020, The Author(s).
PY - 2020
Y1 - 2020
N2 - 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.
AB - 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.
KW - First-Order Logic
KW - First-Order Logic with Recursive Definitions
KW - Heap Verification
KW - Program Logics
KW - Program Verification
UR - http://www.scopus.com/inward/record.url?scp=85084008312&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85084008312&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-44914-8_19
DO - 10.1007/978-3-030-44914-8_19
M3 - Conference contribution
AN - SCOPUS:85084008312
SN - 9783030449131
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 515
EP - 543
BT - Programming 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
A2 - Müller, Peter
PB - Springer
T2 - 29th European Symposium on Programming, ESOP 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020
Y2 - 25 April 2020 through 30 April 2020
ER -