Formally verifying exceptions for low-level code with separation logic
From MaRDI portal
Publication:1683698
DOI10.1016/j.jlamp.2017.09.004zbMath1382.68053OpenAlexW2763243490MaRDI QIDQ1683698
Jesper Bengtson, Marco Paviotti
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
formal verificationseparation logicinteractive theorem provingCoqassemblyexceptionsstep-indexed models
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Uses Software
Cites Work
- Unnamed Item
- Certifying low-level programs with hardware interrupts and preemptive threads
- Toward compositional verification of interruptible OS kernels and device drivers
- Program logic and equivalence in the presence of garbage collection.
- Correctness of data representations involving heap data structures
- Charge!
- High-level separation logic for low-level code
- Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq
- First steps in synthetic guarded domain theory: step-indexing in the topos of trees
- A very modal model of a modern, major, general type system
- BI as an assertion language for mutable data structures
- Impredicative Concurrent Abstract Predicates
- Program Logics for Certified Compilers
- Hoare Logic for Realistically Modelled Machine Code
This page was built for publication: Formally verifying exceptions for low-level code with separation logic
