Deep Specifications and Certified Abstraction Layers

DOI10.1145/2676726.2676975zbMath1345.68107OpenAlexW2095770127MaRDI QIDQ2819848

Ronghui Gu, Yu Guo, Haozhong Zhang, Xiongnan Wu, Shu-Chun Weng, Tahina Ramananandro, Jérémie Koenig, Zhong Shao

Publication date: 29 September 2016

Published in: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2676726.2676975

zbMATH Keywords

modularityprogram verificationabstraction layercertified OS kernelscertified compilersdeep specification

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (9)

Connecting Higher-Order Separation Logic to a First-Order Outside World ⋮ ANF preserves dependent types up to extensional equality ⋮ Toward compositional verification of interruptible OS kernels and device drivers ⋮ System-level non-interference of constant-time cryptography. I: Model ⋮ Formal reasoning under cached address translation ⋮ Unnamed Item ⋮ Verified software units ⋮ Unnamed Item ⋮ Cogent: uniqueness types and certifying compilation

Uses Software

• Coq

This page was built for publication: Deep Specifications and Certified Abstraction Layers