Author

Zhong Shao

Abstract

Certified software consists of a machine-executable program plus a formal machine-checkable proof that the software is free of bugs with respect to a claim of dependability. The conventional wisdom is that certified software will never be feasible because the dependability of any real software must also rely on that of its underlying operating system and execution environment which are too low-level 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, local reasoning and separation logic, domain-specific logics and certified linking, and certified or certifying compilation. In this article, I give an overview of this exciting new field, focusing on both foundational ideas and key insights that make certified software differ from traditional program verification systems. I will also describe several exciting recent advances and challenging open problems.

Published

• In Communications of the ACM, 53(12), pages 56-66, December 2010. [PDF]