CheckFence is a SAT-based formal verification tool that analyzes C code implementing concurrent data types on multiprocessors (concurrent queues, sets etc.) with respect to a selected memory model. CheckFence soundly verifies or falsifies the implementation for individual tests supplied by the user, covering all possible instruction interleavings and reorderings. CheckFence does not require formal specifications or annotations, but mines a specification directly from the C code (either from the implementation under test, or from a reference implementation). CheckFence currently supports a limited but reasonable subset of C, as required for typical implementations. This subset includes conditionals, loops, pointers, arrays, structures, function calls, locks, and dynamic memory allocation. CheckFence lets the user specify the desired memory model in an axiomatic format. If a test fails, CheckFence provides an HTML-formatted counterexample trace that displays various views of the execution and can be navigated using hyperlinks.

References in zbMATH (referenced in 15 articles )

Showing results 1 to 15 of 15.
Sorted by year (citations)

  1. Cheng, Steven; Higham, Lisa; Kawash, Jalal: Partition consistency. A case study in modeling systems with weak memory consistency and proving correctness of their implementations (2014)
  2. Malkis, Alexander; Banerjee, Anindya: On automation in the verification of software barriers: experience report (2014)
  3. Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Chen, Yu-Fang; Leonardsson, Carl; Rezine, Ahmed: Memorax, a precise and sound tool for automatic fence insertion under TSO (2013)
  4. Alglave, Jade; Kroening, Daniel; Nimal, Vincent; Tautschnig, Michael: Software verification for weak memory via program transformation (2013)
  5. Dongol, Brijesh; Travkin, Oleg; Derrick, John; Wehrheim, Heike: A high-level semantics for program execution under total store order memory (2013)
  6. Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Chen, Yu-Fang; Leonardsson, Carl; Rezine, Ahmed: Counter-example guided fence insertion under TSO (2012)
  7. Dubrovin, Jori; Junttila, Tommi; Heljanko, Keijo: Exploiting step semantics for efficient bounded model checking of asynchronous systems (2012)
  8. Burnim, Jabob; Sen, Koushik; Stergiou, Christos: Sound and complete monitoring of sequential consistency for relaxed memory models (2011)
  9. Guerraoui, Rachid; Henzinger, Thomas A.; Singh, Vasu: Verification of STM on relaxed memory models (2011)
  10. Wang, Chao; Kundu, Sudipta; Limaye, Rhishikesh; Ganai, Malay; Gupta, Aarti: Symbolic predictive analysis for concurrent programs (2011)
  11. Guerraoui, Rachid; Henzinger, Thomas A.; Singh, Vasu: Model checking transactional memories (2010)
  12. Guerraoui, Rachid; Henzinger, Thomas A.; Singh, Vasu: Software transactional memory on relaxed memory models (2009)
  13. Burckhardt, Sebastian; Musuvathi, Madanlal: Effective program verification for relaxed memory models (2008)
  14. Aspinall, David; Ševčík, Jaroslav: Formalising Java’s data race free guarantee (2007)
  15. Huynh, Thuan Quang; Roychoudhury, Abhik: Memory model sensitive bytecode verification (2007)