swMATH ID: 9939
Software Authors: Burckhardt, S., Alur, R., Martin, M.K.
Description: 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.
Homepage: http://checkfence.sourceforge.net/
Related Software: veriSoft; SPIN; UMM; CBMC; Java Grande; Antichains; Velodrome; Atomizer; MAGIC; ISP; GitHub; LLVM; Weak2SC; Lazy-CSeq; Jahob; VACID-0; PARSEC; Boogie; VCC; SPASS+T
Cited in: 18 Documents

Citations by Year