News for hackers. Stuff that matters.

A comment on Rules for Writing Safety Critical Code (2006). Parent comment

Re:Rules for Writing Safety Critical Code (2006) by mos_basik on Friday November 04, 2016 @11:38AM (#12873404)
Gerard Holzmann is the main author of the formal software verification tool "spin" as well as the owner of spinroot.com. I took a class on formal verification under him at Caltech.
[ Parent | on HN ]
Re:Rules for Writing Safety Critical Code (2006) by 4ad on Friday November 04, 2016 @11:44AM (#12873459)
As an anecdote, spin was used in Plan 9 to validate the kernel scheduler and the IL network protocol. It was also used to validate a very early version of the Go scheduler.
[ Parent | on HN ]
Re:Rules for Writing Safety Critical Code (2006) by mturmon on Friday November 04, 2016 @12:01PM (#12873585)
Gerard is an ACM Fellow and a member of the NAE, and has been a leader in reliable software for NASA since he came to JPL from Bell Labs.
[ Parent | on HN ]
Re:Rules for Writing Safety Critical Code (2006) by nstj on Friday November 04, 2016 @02:59PM (#12874998)
I probably should have clicked around a bit to determine that he is the owner of that site :)
[ Parent | on HN ]