flat assembler
Message board for the users of flat assembler.

Index > Heap > 30 people-years to certify 7500 lines of code bug free

Goto page Previous  1, 2
Thread Post new topic Reply to topic
Your code has a bug

Joined: 06 May 2005
Posts: 4633
Location: Argentina
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 Sad

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? Razz *

*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).
Post 27 Sep 2009, 23:46
View user's profile Send private message Reply with quote

Joined: 25 Sep 2003
Posts: 2141
Location: Estonia
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 Wink
Post 28 Sep 2009, 14:34
View user's profile Send private message Visit poster's website Yahoo Messenger MSN Messenger Reply with quote
Display posts from previous:
Post new topic Reply to topic

Jump to:  
Goto page Previous  1, 2

< Last Thread | Next Thread >
Forum Rules:
You cannot post new topics in this forum
You cannot reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot vote in polls in this forum
You can attach files in this forum
You can download files in this forum

Copyright © 1999-2020, Tomasz Grysztar.

Powered by rwasa.