A first-order logic with frames

DOI10.1007/978-3-030-44914-8_19MaRDI QIDQ5041109zbMATH OpenOpenAlexFDO

Authors Adithya Murali, Lucas Peña, Christof Löding, Parthasarathy Madhusudan

Publication date 13 October 2022

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

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

first-order logicfirst-order logic with recursive definitionsheap verificationprogram logicsprogram verification

Mathematics Subject Classification ID

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

Recommendations

• The relationship between separation logic and implicit dynamic frames
• The relationship between separation logic and implicit dynamic frames
• Frame inference for inductive entailment proofs in separation logic
• Relational logic with framing and hypotheses
• Foundations of Software Science and Computational Structures

Cites work

• A Basis for Verifying Multi-threaded Programs
• A semantics for concurrent separation logic
• Analysis of algorithms on threaded trees
• Automated cyclic entailment proofs in separation logic
• Automated mutual explicit induction proof in separation logic
• Coming to terms with quantified reasoning
• Dafny: an automatic program verifier for functional correctness
• Decision procedures for algebraic data types with abstractions
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• GRASShopper
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• Local reasoning for global invariants. I: Region logic
• Local reasoning for global invariants. II: Dynamic boundaries
• Modular reasoning about heap paths via effectively propositional formulas
• Programming Languages and Systems
• Recursive proofs for inductive tree data-structures
• Separation and information hiding
• Separation logic and abstraction
• Separation logic modulo theories
• Separation logics and modalities: a survey
• Smallfoot
• The dynamic frames theory
• The relationship between separation logic and implicit dynamic frames
• Tractable Reasoning in a Fragment of Separation Logic

Cited in

(5)

• The relationship between separation logic and implicit dynamic frames
• Frame problem in dynamic logic
• scientific article; zbMATH DE number 408805 (Why is no real title available?)
• Ordered Fragments of First-Order Logic
• Dynamic separation logic

Describes a project that uses

Uses Software

• Smallfoot
• GRASShopper
• Dafny
• VAMPIRE

This page was built for publication: A first-order logic with frames

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5041109)