Message board for the users of flat assembler.
> Heap > 30 people-years to certify 7500 lines of code bug free
Goto page Previous 1, 2
Yes, I would also like to know, even in a more general way but unfortunately there is very few info about formal verification outside functional programming languages
The best thing (in my ultra humble opinion) I've found so far was this: http://www.cse.chalmers.se/edu/course/TDA566/schedule.html . It covers Java though... But at least it is not based on Haskell or things like that.
If someone can share more info and talk about your own experience in the subject it would be great.
Perhaps for exercising ourselves we should try verifying fasm formally to make it the best assembler for critical mission software? *
*Though seriously, this would be a good advertisement for fasm.
PS: About the time, note that the automatic proving takes a lot of COMPUTATION time, so don't be scared so much, perhaps the 25-30 "person years" (what this exactly means?), included the time Isabelle took to verify the theorems (NP-Complete problem if I recall correctly).
|27 Sep 2009, 23:46||
I think ASM has many constructs and implementations (lets call them magic) that aren't eligible for proving.
The whitepaper I pointed out, showed that it falls short when dealing with new type of NICs and videocards, where you upload some program in RAM to be executed & stuff... That's too much for this kind of project.
It needs a *normal* approach for a problem
|28 Sep 2009, 14:34||
|Goto page Previous 1, 2
< Last Thread | Next Thread >
Copyright © 1999-2020, Tomasz Grysztar.
Powered by rwasa.