Sciweavers

TPHOL
2007
IEEE

Using XCAP to Certify Realistic Systems Code: Machine Context Management

14 years 4 months ago
Using XCAP to Certify Realistic Systems Code: Machine Context Management
Formal, modular, and mechanized verification of realistic systems code is desirable but challenging. Verification of machine context management (a basis of multi-tasking) is one representative example. With context operations occurring hundreds to thousands of times per second on every computer, their correctness deserves careful examination. Given the small and stable code bases, it is a common misunderstanding that the context management code is suitable for informal scrutiny and testing. Unfortunately, after being extensively studied and used for decades, it still proves to be a common source of bugs and confusion. Yet its verification remains difficult due to the machine-level detail, irregular patterns of control flows, and rich application scenarios. This paper reports our experience applying XCAP—a recent theoretical verification framework—to certify a realistic x86 implementation of machine context management. XCAP supports expressive and modular logical specificatio...
Zhaozhong Ni, Dachuan Yu, Zhong Shao
Added 04 Jun 2010
Updated 04 Jun 2010
Type Conference
Year 2007
Where TPHOL
Authors Zhaozhong Ni, Dachuan Yu, Zhong Shao
Comments (0)