Skip to content
Snippets Groups Projects
Commit 4fcbb21a authored by David Renshaw's avatar David Renshaw
Browse files

tweak wording in readme

parent 2b026cc7
Branches
No related tags found
No related merge requests found
...@@ -7,15 +7,15 @@ Seer is a fork of [miri](https://github.com/solson/miri) ...@@ -7,15 +7,15 @@ Seer is a fork of [miri](https://github.com/solson/miri)
that adds support for symbolic execution, using that adds support for symbolic execution, using
[z3](https://github.com/Z3Prover/z3) as a solver backend. [z3](https://github.com/Z3Prover/z3) as a solver backend.
Given a program, Seer attempts to exhaustively Given a program written in Rust, Seer attempts to exhaustively
enumerate the possible execution paths through that program. enumerate the possible execution paths through it.
Seer represents program input in a _symbolic_ form To achieve this, Seer represents the program's input in a _symbolic_ form,
and maintains a set of constraints on it. maintaining a set of constraints on it.
When Seer reaches a branching point in the program, it When Seer reaches a branch point in the program, it
invokes its solver backend to compute which branches invokes its solver backend to compute which continuations
are feasible given the current constraints. The feasible are possible given the current constraints. The possible
branches are then enqueued for exploration, augmented with the continuations are then enqueued for exploration, augmented with the
new constraints learned from the branching condition. respective new constraints learned from the branch condition.
Seer considers any bytes read in through `::std::io::stdin()` Seer considers any bytes read in through `::std::io::stdin()`
as symbolic input. This means that once as symbolic input. This means that once
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment