Paper Info
Title
Modular Development of Certified System Software
Abstract
Certified software consists of a machine executable program plus a rigorous formal proof (checkable by computer) that the software is free of bugs with respect to a particular specification. The conventional wisdom is that certified software will never be practical because any real software must also rely on the underlying operating system which is too low-level and complex to be verifiable. In recent years, however, there have been many advances in the theory and engineering of mechanized proof systems applied to verification of low-level code, including proof-carrying code, certified assembly programming, logic-based type system, and certified or certifying compilation. In this talk, I will give an overview of this exciting new area, focusing on both foundational ideas and key insights that make the work on certified software differ from traditional style program verification. I will also describe several recent work on building certified thread implementation, interrupt handlers, stack-based control libraries, garbage collectors, and OS bootloaders.
Year
DOI
Venue
2009
10.1109/TASE.2009.49
TASE
Keywords
Field
DocType
modular development,interrupt handler,proof-carrying code,real software,certified software,certified code,certified assembly programming,multi-threading,mechanized proof system,operating systems (computers),logic-based type system,operating system,recent work,os bootloader,certification,interrupts,machine-checkable proofs,machine executable program,stack-based control library,program assemblers,modular verification,dependable software,certified system software,certified thread implementation,program verification,formal specification,low-level code,operating systems,logic programming,computer science,software engineering,assembly,garbage collector,multi threading,type system,computer bugs
System software,Programming language,Software engineering,Computer science,Software bug,Real-time computing,Formal specification,Software system,Software,Software construction,Software development,Software verification
Conference
ISBN
Citations 
PageRank 
978-0-7695-3757-3
0
0.34
References 
Authors
1
1
Name
Order
Citations
PageRank
Zhong Shao189768.80