Certified software

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 is 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, certified linking of heterogeneous components, 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 the work on certified software differ from traditional program verification systems. I will also describe ...

• Type: Journal
• Year: 2010
• Where: CACM
• Authors: Zhong Shao
• Keywords: Applied Computing, CACM 2010, Formal Machine-checkable Proof, Software, Traditional Program Verification