|This article is the subject of an educational assignment supported by Wikipedia Ambassadors through the India Education Program.|
|WikiProject Computer science||(Rated Start-class, High-importance)|
- 1 Untitled
- 2 "Verification" redirect?
- 3 Automated theorem proving?
- 4 category in area of software verification
- 5 Merge from Program verification
- 6 Actual use
- 7 Correctness of a system
- 8 Tool support
- 9 Third possible approach: Type Systems
- 10 Verifiability redirect
- 11 Formal Verification of Operating System
Sorry 184.108.40.206, 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...
I think we need at least one example here. - Furrykef 00:46, 30 Jul 2004 (UTC)
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)
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.
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
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)
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)
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.
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)
Only a small set of verification tools/environments were mentioned here. Conspicuous in its absence is the PVS verification environment. Rather than inviting anyone to place their pet tool (whether proprietary or open-source), may I suggest that only tools appearing in the open refereed literature (based on a search of IEEE Explore, ACM's Digital Library, or tool names appearing in DBLP) be included in a bulleted list with a one-sentence explanation as to what makes each tool unique, along with an in-line reference to a tutorial pertaining to that tool. Vonkje (talk) 15:39, 14 May 2008 (UTC)
Even better, the article should simply link to articles about automatic theorem proving, interactive theorem proving, and model checking. Program verification should also be broken out into a separate article. This article should just explain conceptually the idea of applying mathematics to reason about systems, and guide the reader to the areas likely to be of interest. (Erniecohen (talk) 13:49, 12 October 2012 (UTC))
Third possible approach: Type Systems
Besides model checking and theorem proving there is also a third approach: type systems for verifying specific properties of programs —Preceding unsigned comment added by 220.127.116.11 (talk) 08:46, 31 August 2008 (UTC)
Formal Verification of Operating System
This article currently contains a section titled "Formal Verification of Operating System" which contains the following:
- The safety of a computer is dependent on the safety of the kernel. Functional correctness in case of a kernel means the implementation completely follows the high level abstract specifications. The common approach for ensuring safety of a kernel is by reducing the amount of privileged code thus reducing the exposure to bugs. We can guarantee absence of bugs by mathematically proving that the kernel implementation follows formal specifications and that it is free from programmer induced defects.
This does not make sense - for example "safety of a computer" is unclear, but where that term has been used in real life (try googling it) it's not directly related to terms such as "Type safety" used in the cited paper.
My knowledge of formal verification (despite having worked in closely related fields) is insufficient for me to easily comprehend the cited paper, so I don't know whether the above text can be fixed (e.g. by making changes such as replacing "safety" with "integrity"). I propose deleting the section and adding a reference to the ACM paper to the L4 microkernel family article. DexDor (talk) 22:38, 7 November 2011 (UTC)