46 ms·
I'm no expert but the way I understand it is you are mathematically proving certain things about the software. Basically you prove that there won't be a divisio
by quantumhobbit 10y ago
I'm no expert but the way I understand it is you are mathematically proving certain things about the software. Basically you prove that there won't be a division by zero or buffer overflow or whatever in a certain function.
Usually there are extensions to programming languages that let you annotate these proofs and software can check it for you.
Like with unit tests you only get these assurances if you write out the proofs. Historically writing them has been really time consuming, but the paper claims it is getting much more convenient.
- johncolanduoni 10y agoSome of the methods they list (like SAT solvers and model checkers) mostly obviate the actual proving part for simple statements. Instead you only need to input what you want to prove, and the computer attempts to find a proof or disproof. For many of the things you would want to prove in software, this is sufficient.