We describe semi-automatic verification of the software barrier synchronization primitive. We improve the state of the art in automatically proving the correctness of software barrier algorithms. On one hand, we show the best possible results in proving correctness with off-the-shelf automatic verification tools, in passing improving the capabilities of one of these tools. On the other hand, for each algorithm we show a slightly more complicated version that still lies beyond the current automatic verification frontier. We have automatically verified a central barrier, a static tree barrier, a combining tree barrier, a dissemination barrier, a tournament barrier, a C implementation of a barrier, and a barrier with its client.