Sign In

Communications of the ACM

Research Archive


Archives

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

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

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…