I can't give a good, covering answer without writing a wall of text, sorry in advance.
CBMC and KLEE try to statically verify assertions in one of three outcomes:
1. Verified: No counter-example was found, that breaks the assertion(s).
2. Rejected: A counter-example was found, that makes an assertion false.
3. Tool runs forever or exhausts system resources.
That means, any test/verification you can do at runtime, can be determined statically. You can use modal logics, automata, everything within practical limits.
The modeling language is also just C, which simplifies things HUGELY.
A very simple example can be found here: https://github.com/kokke/tiny-regex-c/blob/master/formal_ver... (note, this has no specific assertions, only the ones inserted automatically by the tool, to check for run-time errors like zero division, array out of bounds etc.).
So would I!
I can't give a good, covering answer without writing a wall of text, sorry in advance.
CBMC and KLEE try to statically verify assertions in one of three outcomes:
1. Verified: No counter-example was found, that breaks the assertion(s).
2. Rejected: A counter-example was found, that makes an assertion false.
3. Tool runs forever or exhausts system resources.
That means, any test/verification you can do at runtime, can be determined statically. You can use modal logics, automata, everything within practical limits.
The modeling language is also just C, which simplifies things HUGELY.
A very simple example can be found here: https://github.com/kokke/tiny-regex-c/blob/master/formal_ver... (note, this has no specific assertions, only the ones inserted automatically by the tool, to check for run-time errors like zero division, array out of bounds etc.).
For more involved examples, see https://www.cprover.org/cbmc/applications/ or https://klee-se.org/publications/
That's fantastic, thanks! These sound like astounding systems.
1 reply →