Verification Challenges

You would like to do some formal verification of C code? Or you would like a challenge for your formal-verification tool? Either way, here you go!
 
 
 

1. Stupid RCU Tricks: rcutorture Catches an RCU Bug, also known as Verification Challenge 1.
   
2. Verification Challenge 2: RCU NO_HZ_FULL_SYSIDLE.
   
3. Verification Challenge 3: cbmc.
   
4. Verification Challenge 4: Tiny RCU.
   
5. Verification Challenge 5: Uses of RCU.
   
6. Verification Challenge 6: Linux-Kernel Tree RCU.
   
7. Verification Challenge 7: Heavy Modifications to Linux-Kernel Tree RCU.