Connecting Higher-Order Separation Logic to a First-Order Outside World

DOI10.1007/978-3-030-44914-8_16OpenAlexW3016373772MaRDI QIDQ5041105

Andrew W. Appel, Wolf Honoré, William Mansky

Publication date: 13 October 2022

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

Full work available at URL: https://doi.org/10.1007/978-3-030-44914-8_16

zbMATH Keywords

formal verificationmodular verificationVSTCertiKOSinteraction treesverifying communication

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

• Toolchain
• seL4
• CertiKOS

Cites Work

• Resources, concurrency, and local reasoning
• Sound, Modular and Compositional Verification of the Input/Output Behavior of Programs
• Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity
• Deep Specifications and Certified Abstraction Layers
• Views
• Subjective auxiliary state for coarse-grained concurrency
• Higher-order ghost state
• Verified Characteristic Formulae for CakeML
• Program Logics for Certified Compilers

This page was built for publication: Connecting Higher-Order Separation Logic to a First-Order Outside World