Skip to content

Commit

Permalink
Update README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
wintered authored Oct 20, 2024
1 parent fbf1de8 commit ee601f4
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,7 @@ Perhaps more importantly anything are the assurances that we gained.

### Evolution (Nov 2016 - Mar 2024)
The small scope hyothesis states that "almost all interesting bahavior of software is observable on small inputs" [Jackson '04].
Studying 1,000+ bugs in Z3 and cvc4 (c.f. [OOPSLA '20](https://dl.acm.org/doi/abs/10.1145/3428261)), we observed that the small scope hyothesis holds for SMT solvers.
Studying 1,000+ bugs in Z3 and cvc4 (c.f. [OOPSLA '20](https://dl.acm.org/doi/abs/10.1145/3428261) Fig.15), we observed that the small scope hyothesis holds for SMT solvers.
We can hence approach questions such as: *Have we tested SMT solvers enough? How did SMT solver's correctness and performance evolve*? To approach these questions,
we ran a large-scale experiment with all releases of Z3 and CVC4/cvc5 from the last 6 years (61 releases). We then ran ET with grammars
of each theory tracking the number of bugs found and runtime on 1 million formulas.
Expand Down

0 comments on commit ee601f4

Please sign in to comment.