The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

Certified Software

Last modified: Thu Dec 16 16:36:27 2010 GMT.

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] and [PS]

Copyright © 1996-2016 The FLINT Group <flint at cs dot yale dot edu>
Yale University Department of Computer Science
Validate this page
colophon