Formally verifying exceptions for low-level code with separation logic

DOI10.1016/J.JLAMP.2017.09.004MaRDI QIDQ1683698zbMATH OpenOpenAlexFDO

Authors Marco Paviotti, Jesper Bengtson

Publication date 1 December 2017

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://kar.kent.ac.uk/67658/2/jlamp.pdf

zbMATH Keywords

separation logicCoqformal verificationinteractive theorem provingassemblyexceptionsstep-indexed models

Mathematics Subject Classification ID

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

Recommendations

• High-level separation logic for low-level code
• Types, bytes, and separation logic
• Abstracting Allocation
• Certifying low-level programs with hardware interrupts and preemptive threads
• Separation Logic for Small-Step cminor

Cites work

• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• A very modal model of a modern, major, general type system
• BI as an assertion language for mutable data structures
• Certifying low-level programs with hardware interrupts and preemptive threads
• Charge! A framework for higher-order separation logic in Coq
• Correctness of data representations involving heap data structures
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• High-level separation logic for low-level code
• Hoare Logic for Realistically Modelled Machine Code
• Impredicative concurrent abstract predicates
• Program logic and equivalence in the presence of garbage collection.
• Program logics for certified compilers
• Toward compositional verification of interruptible OS kernels and device drivers
• Verifying object-oriented programs with higher-order separation logic in Coq

Cited in

(1)

• Certifying low-level programs with hardware interrupts and preemptive threads

Describes a project that uses

Uses Software

• Charge!
• Toolchain
• Coq

This page was built for publication: Formally verifying exceptions for low-level code with separation logic

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