Text Size
- Home
-
News
Advanced computing news from Communications of the ACM, other ACM resources, and from around the Web.
- Blogs
- Opinion
-
Browse by Subject
Recent articles from Communications organized into categories that encompass the broad scope of computing.
-
Magazine Archive
-
Careers
Jump-start your career with information on trends, opportunities and jobs – in both industry and academia.
- ACM Resources
-
Subscribe
Receive the benefits of ACM membership with a subscription to its flagship publication, Communications of the ACM.
Home » Magazine Archive » 2010 » No. 6 » seL4: Formal Verification of an Operating-System Kernel » Abstract
Research highlights
seL4: Formal Verification of an Operating-System Kernel
![[article image]](/system/assets/0000/2985/052010_iStock_seL4.large.jpg?1274363741&1274363741 "software illustration")
Credit: iStockPhoto.com
We report on the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its C implementation. We assume correctness of compiler, assembly code, hardware, and boot code.
Read the Full Article:
Tools For Readers
Text Size
Related ACM Resources
Conferences:
- ISMM 2012: International Symposium on Memory Management - June 15 – 16, 2012; Beijing, China
Courses:
- Microsoft Office PowerPoint 2007: Level 2 (Second Edition) - Design Microsoft Office PowerPoint 2007 presentations with high-quality sound and visual enhancements to better meet the expectations of media savvy audiences while effectively making your …
About Communications |
Join ACM 
|
Renew |
Subscribe |
Sign In |
For Authors |
For Advertisers |
Privacy |
Site Map |
Help |
Contact Us |
Mobile Site
Copyright © 2012 by the ACM. All rights reserved.