Re: Follow-up on Holzmann@JPL, Coverity and Tecgraf tools...
[
Date Prev][
Date Next][
Thread Prev][
Thread Next]
[
Date Index]
[
Thread Index]
- Subject: Re: Follow-up on Holzmann@JPL, Coverity and Tecgraf tools...
- From: Thorkil Naur <naur@...>
- Date: 2019年5月26日 20:12:32 +0200
Hello,
On Sun, May 26, 2019 at 08:36:27PM +0930, sur-behoffski wrote:
> ...
> [I'm simply working off of the one presentation by Gerald Holzmann in
> making up this description... if I am wrong, corrections would be very
> welcome.]
The details provided in
Mars Code
By Gerard J. Holzmann
Communications of the ACM, February 2014, Vol. 57 No. 2, Pages 64-73
may be useful. Noting, by the way, that the considerably more complex
example of model checking described in that paper was incorrect: See my
letter to the editor
Code That Missed Mars
Communications of the ACM, April 2014, Vol. 57 No. 4, Page 9
and Holzmanns detailed analysis
http://spinroot.com/dcas/index.html
> ...
Best regards
Thorkil Naur