tis-interpreter also has an open-source foundation, which is Frama-C (http://www.frama-c.com http://www.frama-c.com). Both share some common code. Their purpos

tis-interpreter also has an open-source foundation, which is Frama-C (http://www.frama-c.com http://www.frama-c.com). Both share some common code. Their purpose is not exactly the same as RV-Match's; they are more concerned with soundness and absence of run-time errors (as well as other properties and analyses), while RV-Match is a bug detection tool, focusing on not having false positives. It's important to realize the difference when comparing such kinds of tools. Depending on the situation, one is more appropriate than the other, but in some cases the results may be complementary (as in RV-Match's comparison, where the reported bugs were different for each of them), so if there's already some effort to try one of them (plus the *San's from LLVM), it may be worth trying the others as well. Every bit of help is welcome when dealing with a language such as C. Disclaimer: I work with Frama-C.