3 ms·
I meant to point out formal verification is used in the industry quite a bit (not in aviation alone). 1. Replacing testing with formal verification at Intel (2
by cscurmudgeon 11y ago
I meant to point out formal verification is used in the industry quite a bit (not in aviation alone).
1. Replacing testing with formal verification at Intel (2009)
http://link.springer.com/chapter/10.1007/978-3-642-02658-4_32 http://link.springer.com/chapter/10.1007/978-3-642-02658-4_3...
2. Fifteen years of formal property verification at Intel (2008)
http://link.springer.com/chapter/10.1007/978-3-540-69850-0_8 http://link.springer.com/chapter/10.1007/978-3-540-69850-0_8
3. seL4: formal verification of an OS kernel
http://dl.acm.org/citation.cfm?id=1629596 http://dl.acm.org/citation.cfm?id=1629596
There is such a big need that DARPA has even come up with a contest.
http://www.darpa.mil/program/crowd-sourced-formal-verification http://www.darpa.mil/program/crowd-sourced-formal-verificati...
I could go on, but I would rather not spend my time combating FUD and the general incivility here.
- seanmcdirmid 11y agoFormal verification is used a lot, but it is not a rule and definitely not a requirement by the FAA for aircraft certification. The idea that formal verification would be obviously necessary for the logic of a self-driving car is what was being challenged here. You could call that FUD, but you obviously have an agenda to push, I guess.
- cscurmudgeon 11y ago> not a requirement by the FAA for aircraft certification. I never said that. Where did you get that? > Safety critical systems need a degree of auditing and testing, to be sure, but formal proofs have never been a requirement since they aren't that practical. (emphasis mine) I was challenging this idea. Are systems for self-driving cars the only safety critical systems? What about Intel manufactured chips used in those same cars and flights and a gazillion other devices? You have an agenda to push and got called out on facts :) Have a good day. (Someone just went around down voting my other posts. Not you)
- seanmcdirmid 11y agoI guess it depends on how you interpret "that", which I meant to refer to "requirement" (they are not practical enough to be a requirement). But I guess I should have been more clear in my sentence structure.
- cscurmudgeon 11y agoStill not clear but we will leave it here :) Btw, I use both deep learning and knowledge based systems in my work (but not formal verification) but don't like advertising that goes in AI by academics from all camps(don't want another AI winter).
- seanmcdirmid 11y agoFair enough. I have no skin in this game since I'm a PL researcher...
- raverbashing 11y agoIntel uses verification after they fumbled the Pentium FPU, verifying silicon is a good idea (also it's complex but doable) Now good luck verifying a machine learning system beyond the basics.
- cscurmudgeon 11y agoUmm that is the point being made ...