Automatic Verification of Software Barriers

Experiments were conducted with Jahob revision 2503 (with backends MONA 1.4-13, Z3 2.19, CVC3 2.2-13), Boogie version 2.2.30705.1126 from 2012-10-22 (with backend Z3 4.3.0 from 2012-11-11), VCC version 2.3.809.0 (which came with its own versions of Boogie and Z3), and Spin 6.1.0.

Central barrier

Tree-based barriers

Static tree barrier

Combining tree barrier

Array-based barriers



Real C code

Barrier on TSO

Barrier with its client