Talk:Formal verification

From Wikipedia, the free encyclopedia
Jump to: navigation, search
WikiProject Computer science (Rated Start-class, High-importance)
WikiProject icon This article is within the scope of WikiProject Computer science, a collaborative effort to improve the coverage of Computer science related articles on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.
Start-Class article Start  This article has been rated as Start-Class on the project's quality scale.
 High  This article has been rated as High-importance on the project's importance scale.
 

Untitled[edit]

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)

"Verification" redirect?[edit]

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?[edit]

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[edit]

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[edit]

Should be a section here. Ripper234 20:45, 2 April 2006 (UTC)

Done. -- Beland 00:31, 2 May 2006 (UTC)

Actual use[edit]

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)

Correctness of a system[edit]

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)

Tool support[edit]

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[edit]

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 79.240.84.233 (talk) 08:46, 31 August 2008 (UTC)

Verifiability redirect[edit]

Verifiability should not redirect here. As used in the social sciences, this term has nothing to do with formal verification. 210.54.98.199 (talk) 20:01, 15 September 2008 (UTC)

Formal Verification of Operating System[edit]

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)

I've removed the section referred to above and added a ref to the cited paper to the lead (instead of adding to seL4 article). DexDor (talk) 07:42, 9 November 2011 (UTC)