Communications of the ACM
Research Archive
The Research archive provides access to all Research articles published in past issues of Communications of the ACM.
June 2010
From Communications of the ACM
Technical Perspective: Learning To Do Program Verification
When you decide to use a piece of software, how do you know it will do what you need it to do? Will it be safe to run? Will it interfere with other software you already have…
From Communications of the ACM
Asserting and Checking Determinism For Multithreaded Programs
The trend towards processors with more and more parallel cores is increasing the need for software that can take advantage of parallelism. Writing correct…
From Communications of the ACM
Technical Perspective: Building Confidence in Multicore Software
Surprises may be fun in real life, but not so in software. One approach to avoiding surprises in software is to establish its functional correctness, either by construction…
From Communications of the ACM
seL4: Formal Verification of an Operating-System Kernel
We report on the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its C implementation. We assume correctness of compiler, assembly code, hardware, and boot code.