silviu andrica a écrit :
>
>
> Hello,
> I am very new to Ocaml, this is my first day, and I wanted to know
> if it is possible to prove correctness of a multi-threaded application
> written in Ocaml.

Hello.

I'm having the same issue.

You can perhaps have a look at Jean-Christophe Filliâtre web page.
There's Ocaml proven software there:

http://www.lri.fr/~filliatr/software.en.html

> Basically, I want to check that a multi-threaded implementation of an
> algorithm that detects cycles in a dynamically changing graph, actually
> detects the cycles. Also, the algorithm prevents previously detected
> cycles from happening by not allowing certain edges to be added. And I
> want to check that this property also holds.

But as far as I know, proving multi-threaded programs is quite hectic,
and rather difficult.

> Thank you and I hope you can help me,
> Silviu ANDRICA.

If you make any progress on that one, please let me know.

--
Guillaume Yziquel
http://yziquel.homelinux.org/

•  5
  New Members