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`.
3 questions
2
votes
1
answer
167
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 ...
- 313
12
votes
1
answer
88
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
414
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