Modular verification of preemptive OS kernels

DOI10.1145/2034773.2034827zbMath1323.68195OpenAlexW4248931912MaRDI QIDQ5176991

Hongseok Yang, Alexey Gotsman

Publication date: 5 March 2015

Published in: Proceedings of the 16th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL: https://ora.ox.ac.uk/objects/uuid:f3f2d73b-aa35-4937-851a-ed4fdb41c1bc

zbMATH Keywords

verificationschedulingconcurrencymodularity

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of operating systems (68N25) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

System-level non-interference of constant-time cryptography. I: Model ⋮ Precision and the Conjunction Rule in Concurrent Separation Logic

This page was built for publication: Modular verification of preemptive OS kernels