Is there a Model Checking software (like Java Path Finder) but for C#? [closed]

Question

Closed. This question does not meet Stack Overflow guidelines. It is not currently accepting answers.

---

Questions asking us to recommend or find a tool, library or favorite off-site resource are off-topic for Stack Overflow as they tend to attract opinionated answers and spam. Instead, describe the problem and what has been done so far to solve it.

Closed 8 years ago.

Improve this question

<EDIT> About this question being off-topic and too opinion-based, I'll try to be more clear. My goal was to undestand if such a tool existed, I was not interested in opinions about what was the best one. At the time I wrote this question I spent quite a good amount of time searching the internet and found just old dead projects but such a tool for java existed and I couldn't belive there were nothing for c#. I think this question is related to programming (code verification), and it is not really asking for an opinion. Also, it's still not easy to find this information and I think my answer could help saving someone's time. That said, I'm not an expert of stackoverflow, if you still think the question/answer does not fit the site feel free to delete it. </EDIT>

I've found Moonwalker http://fmt.cs.utwente.nl/tools/moonwalker/ but the last update has been done in 2009 and i don't think it supports .net4.5 (and it's poorly documented).

The answer to this question propose CodeContracts as a model checking tool Model checking tool c# but I've tried using it and I don't think it really is a model checker, not in the same way Java Path Finder for Java is. Im i worng? Can it be used like JPF?

I need to be able to known if a certain part of code is designed in a way that can deadlock. Let's say it's a school thing and even if I'm sure my code is working I must model check it. (Yes we are allowed and encouraged to look on the internet).

Answer 1

As the user @HighCore said, and after lot of searching i can say that a mature and up-to-date tool like the one I described does not exist.

Answer 2

Model checking refers usually to explicit methods, however symbolic methods are equally advanced and arguably more capable for establishing properties of actual code.

For a Turing complete language, the verification problem is undecidable, so model-checking tools usually accept a less powerful language as input. This implies having to convert your problem to that language, before checking. This is why you have not come across any "C# model checking tool".

Have you looked at Boogie and the C#-like Dafny ? These are (essentially) for annotating with Hoare logic.

Alternatively, you can consider model checking your C# solution after (manually) translating it to Promela, then using SPIN.

Related tools (e.g. C-to-Promela translators) are listed here.