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`.

Filter by
Sorted by
Tagged with
0 votes
0 answers
51 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. ...
Gergely's user avatar
  • 299
1 vote
1 answer
141 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 ...
Daniel Donnelly's user avatar
12 votes
1 answer
73 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 ...
Bruno Le Floch's user avatar
9 votes
3 answers
380 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 ...
Glorfindel's user avatar