0

<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).

Community
  • 1
  • 1
flagg19
  • 1,782
  • 2
  • 22
  • 27
  • 2
    I don't think there's anything like that for .Net. It's not really required because .Net code is short and beautiful and powerful. It doesn't have convoluted hacks that deal with language limitations such as not having `Events` and `Delegates`. Threading and Paralellism and Async are really beautiful in C# 5 due to `Async / await`, which allows multiple async calls to be controlled inside a single `Try/Catch`. – Federico Berasategui Sep 03 '13 at 19:43

2 Answers2

0

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.

flagg19
  • 1,782
  • 2
  • 22
  • 27
0

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.

0 _
  • 10,524
  • 11
  • 77
  • 109