Skip to content

Commit

Permalink
Update formal_verification.md
Browse files Browse the repository at this point in the history
  • Loading branch information
kokke authored Jun 11, 2021
1 parent 711981b commit 2d306a5
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion formal_verification.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ Here is a crude demo of formal verification of tiny-regex. This is a hefty plagi

I am using the [KLEE Symbolic Execution Engine](https://klee.github.io/) and their Docker image here on a Debian-based host.

What this does, is mechanically try and prove the abscence of all run-time errors, memory corruption bugs and other problems by symbolic execution. We mark the inputs as being symbolic, so that the tool knows to use that as the "search space". That means KLEE checks all possible inputs of the form we give it.
What this does, is mechanically try to prove the abscence of all run-time errors, memory corruption bugs and other problems by symbolic execution. We mark the inputs as being symbolic, so that the tool knows to use that as the "search space". That means KLEE checks all possible inputs of the form we give it.

Steps:

Expand Down

0 comments on commit 2d306a5

Please sign in to comment.