2020-02-26 04:29:54 +03:00
|
|
|
What4 is a library for representing symbolic terms and communicating with
|
|
|
|
|
satisfiability and SMT solvers (e.g. Yices and Z3).
|
|
|
|
|
|
2020-07-22 00:11:49 +03:00
|
|
|
It was originally a part of the [Crucible](https://github.com/GaloisInc/crucible)
|
2020-02-26 04:29:54 +03:00
|
|
|
project, but has found use cases that are independent of its original
|
|
|
|
|
purpose as the representation language for the Crucible symbolic
|
|
|
|
|
simulator, and has thus been split out into a separate repository.
|
2020-07-22 00:11:49 +03:00
|
|
|
|
2020-07-22 08:31:15 +03:00
|
|
|
For an overview of What4 and how to use it, please see the
|
2020-07-22 00:11:49 +03:00
|
|
|
package-level [README](what4/README.md).
|
2020-12-15 00:54:31 +03:00
|
|
|
|
|
|
|
|
This material is based upon work supported by the Defense Advanced
|
|
|
|
|
Research Projects Agency (DARPA) under Contract No. HR0011-19-C-0070.
|
|
|
|
|
The views, opinions, and/or findings expressed are those of the
|
|
|
|
|
author(s) and should not be interpreted as representing the official
|
|
|
|
|
views or policies of the Department of Defense or the U.S. Government.
|
