Title: Implementation of Distributed Loop Scheduling Schemes on the TeraGrid
Speaker: Anthony T. Chronopoulos教授, 美国得克萨斯大学 圣安东尼奥分校 计算机系
Time: 3pm, Thursday April 26
Venue: Lecture room, Lab for Computer Science, Level 3 Building #5, Institute of Software, CAS

Abstract

Certified software consists of a machine executable program plus a
rigorous proof (checkable by computer) that the software is free of
bugs with respect to a particular specification. Both the proof and
the specification are written using a general-purpose mathematical
logic, the same logic which all of us use (in reasoning) in our daily
life. The logic is also a programming language: everything written in
logic, including proofs and specifications, is developed using
software known as a proof assistant; they can be mechanically checked
for correctness by a small program known as a proof checker. As long
as the logic we use is consistent, and the specification describes
what the user wants, we can be sure that the underlying software is
free of bugs with respect to the 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 key insights and high-level ideas that make the
work on certified software differ from traditional style program
verification. I will also describe several recent work---done by my
group at Yale---on building certified garbage collectors, OS
bootloader, thread implementation, and stack-based control libraries.