@article{Daum_BK_14, doi = {10.1007/s00165-014-0296-9}, month = oct, paperurl = {https://trustworthy.systems/publications/nicta_full_text/7114.pdf}, journal = {Formal Aspects of Computing}, year = {2014}, keywords = {trustworthy systems; refinement proof; microkernel correctness; isabelle/hol}, volume = {26}, title = {Concerned with the Unprivileged: User Programs in Kernel Refinement}, number = {6}, author = {Daum, Matthias and Billing, Nelson and Klein, Gerwin}, pages = {1205--1229} }