Re: Follow-up on Holzmann@JPL, Coverity and Tecgraf tools...

[Thorkil Naur <naur@...>]

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