Talk:Formal verification
From Wikipedia, the free encyclopedia
Sorry 216.201.222.104, I can't agree with your last edit. formal verif. doesn't "describe" ... but rather "is" ...
And about the link title you changed: I agree it's better english speaking to put it your way but it's missleading that way. I guess it's better to have something slighlty uglier but cleared...
--[[User:Gedeon|Ged (talk)]] 22:21, 20 Jul 2004 (UTC)
I think we need at least one example here. - Furrykef 00:46, 30 Jul 2004 (UTC)
Contents |
[edit] "Verification" redirect?
Why does "Verification" redirect here? The concept of "verification" is not only the purview of Computer Science. Was there ever an article on the more broadly-accepted defitnition of "Verification"? Thanks. --NightMonkey 10:35, Nov 28, 2004 (UTC)
- Vaguely apropos of this, I've started a discussion of the distinction between verification and validation at Talk:Validation#Verification_vs_validation. -- JTN 20:36, 2005 Jun 6 (UTC)
[edit] Automated theorem proving?
I am somehow confused with the tradition to use the term "automated" where something is actually only "computer aided": "automated theorem proving" for proof assistants, "automated programming" for program transformation tools. Some steps are automated, but the whole process is not. If the term "automated" was restricted to cases, where the whole process is automated, it would be more descriptive.
[edit] category in area of software verification
there are too many concepts in area of software verification. who can give me a clear relation or category of this area? I hope the category involves the concepts: software verification, software testing, functional verification, formal verification, whrite box, black box , static analysis, dynamic analysis, model checking, and lint
[edit] Merge from Program verification
Should be a section here. Ripper234 20:45, 2 April 2006 (UTC)
- Support merge of Program verification into the article on Formal verification. These are the same thing. Jon Awbrey 03:34, 19 April 2006 (UTC)
- Support merge of Program verification into the article on Formal verification. These are the same thing. Jimbonkers 16:27, 25 April 2006 (BST)
Done. -- Beland 00:31, 2 May 2006 (UTC)
[edit] Actual use
 |
Please help improve this article or section by expanding it. Further information might be found on the talk page or at requests for expansion. This article has been tagged since January 2007. |
Does anyone know if formal verification is used in any non-academic engineering endeavor, like a nuclear reactor or the Space Shuttle program? -- Beland 00:33, 2 May 2006 (UTC)
The FAA recommends (if not mandates) the use of formal verification for flight control systems. I believe the FDA has similar guidelines concerning formal verification. Staats 08:35, 22 November 2006 (UTC)
[edit] Correctness of a system
A system is an instantiation of a set of algorithms. Algorithms are mathematical entities. Formal verification can prove or disprove the correctness of the mathematical entity (the algorithm). However, it cannot tell whether a particular instance correctly implements the, otherwise correct, algorithms. Therefore, formal verification cannot prove or disprove the correctness of a system.
Two suggestions:
1. The phrase “…the correctness of a system…” should be changed to: “…the correctness of algorithms in systems…”
2. A short explanation should be added, regarding to the difference between the scope of software testing (an actual instance of a system) and formal verification (an algorithm) as explained above.
I would like to have the opinion of the community on this before I edit the article. --Erhasalz 18:09, 2 December 2006 (UTC)
I agree with that. I am aware of no method of applying formal verification directly to code. It's all done with models. Staats 17:03, 7 February 2007 (UTC)
