Questions tagged [verification]
Use this tag with verification that can be either static or dynamic. For a narrower definitions use `static-verification` or `formal-verification`.
4
questions
0
votes
0
answers
53
views
Correcting formally verified results
John Harrison spoke once about checking the results of some peer reviewed mathematical research: he has found bugs in the proofs and even a faulty theorem, which he corrected by giving a formal proof.
...
- 321
2
votes
1
answer
153
views
Does there exists a logical format so that my app can export in that format, and the existing popular proof assistants can take it as input?
I'm creating a "CAS for category theory / homological algebra" in C++ that "supports proofs". Although it is feature creep, I was wondering if there exists a format that my app ...
12
votes
1
answer
77
views
Tools to check correctness of decimal floating point arithmetic
I have implemented (in TeX, but it doesn't matter for this question) a library of functions that evaluate basic arithmetic, as well as some transcendental functions such as cosine, on decimal floating ...
- 502
9
votes
3
answers
399
views
Could proof assistants be used to prove that some piece of code is free of bugs?
Formal verification is
the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of ...
- 731