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.
Is there a Model Checking software (like Java Path Finder) but for C#? [closed]
-
27-06-2022 - |
문제
<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).
해결책
다른 팁
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.