Communications of the ACM
Research Archive
The Research archive provides access to all Research articles published in past issues of Communications of the ACM.
July 2009
From Communications of the ACM
Technical Perspective: The Ultimate Pilot Program
In one scene from The Matrix, two leaders of the human resistance are trapped on the roof of a skyscraper. The only means of escape is by helicopter, which neither can operate. The humans quickly call up a "pilot program" for…
From Communications of the ACM
Apprenticeship Learning For Helicopter Control
Autonomous helicopter flight is widely regarded to be a highly challenging control problem. As helicopters are highly unstable and exhibit complicated dynamical behavior, it is particularly difficult to design controllers that…
From Communications of the ACM
Technical Perspective: A Compiler's Story
In the early 1970s, pioneers like Floyd, Dijkstra, and Hoare argued that programs should be formally specified and proven correct. But for the past 40 years, most of the computer…
From Communications of the ACM
Formal Verification of a Realistic Compiler
This paper reports on the development and formal verification of CompCert, a compiler from Clight (a large subset of the C programming language) to PowerPC assembly code, using the Coq proof assistant both for programming the…