Talk:Formal verification

Untitled

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?

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)

Actual use

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

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

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

Verifiability redirect

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

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)

Automated program repair

I have added a pointer to the (new, Dec 2015) article on Automatic bug fixing to the section on Automated program repair.

However I wonder if the section on Automated program repair should be combined with the article on Automatic bug fixing????

Bill

W102102 (talk) 15:30, 4 January 2016 (UTC)

External links modified

Hello fellow Wikipedians,

I have just modified one external link on Formal verification. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://web.archive.org/web/20150521171234/https://sel4.systems/Docs/seL4-spec.pdf to https://sel4.systems/Docs/seL4-spec.pdf

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

Y An editor has reviewed this edit and fixed any errors that were found.

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 04:26, 4 October 2017 (UTC)

Neutral Point of View

In the "Software" section, it seems like the following statement is too editorial:

A promising type-based verification approach is dependently typed programming, in which the types of functions include (at least part of) those functions' specifications, and type-checking the code establishes its correctness against those specifications. — Preceding unsigned comment added by 71.73.25.5 (talk) 02:01, 26 December 2017 (UTC)

India Education Program course assignment

This article was the subject of an educational assignment supported by Wikipedia Ambassadors through the India Education Program.

The above message was substituted from {{IEP assignment}} by PrimeBOT (talk) on 19:56, 1 February 2023 (UTC)