Skip to content

Commit 02d0a43

Browse files
authored
Update formal_verification.md
1 parent 82cabcd commit 02d0a43

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

formal_verification.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Here is a crude demo of formal verification of tiny-regex. This is a hefty plagi
44

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

7-
What this does, is mechanically try and prove the abscence of all run-time errors, memory corruption bugs and other problems by formally verifying that the code is working properly. 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.
7+
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.
88

99
Steps:
1010

0 commit comments

Comments
 (0)