A First-Order Logic with Frames

DOI10.1007/978-3-030-44914-8_19OpenAlexW3021453356MaRDI QIDQ5041109

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

Publication date: 13 October 2022

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1901.09089

zbMATH Keywords

first-order logicprogram verificationprogram logicsheap verificationfirst-order logic with recursive definitions

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• Dafny
• VAMPIRE
• Smallfoot
• GRASShopper

Cites Work

• Unnamed Item
• Smallfoot
• GRASShopper
• The dynamic frames theory
• A semantics for concurrent separation logic
• Automated mutual explicit induction proof in separation logic
• Separation Logic Modulo Theories
• Recursive proofs for inductive tree data-structures
• The Relationship between Separation Logic and Implicit Dynamic Frames
• Dafny: An Automatic Program Verifier for Functional Correctness
• Tractable Reasoning in a Fragment of Separation Logic
• Separation and information hiding
• A Basis for Verifying Multi-threaded Programs
• Analysis of algorithms on threaded trees
• Separation logics and modalities: a survey
• Automated Cyclic Entailment Proofs in Separation Logic
• Decision procedures for algebraic data types with abstractions
• Separation logic and abstraction
• Coming to terms with quantified reasoning
• Local Reasoning for Global Invariants, Part I
• Local Reasoning for Global Invariants, Part II
• Modular reasoning about heap paths via effectively propositional formulas
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Programming Languages and Systems

This page was built for publication: A First-Order Logic with Frames