tweag / pirouette

Language-generic workbench for building static analysis
MIT License
47 stars 2 forks source link

Use several SMT solvers in parallel #180

Open qaristote opened 1 year ago

qaristote commented 1 year ago

The purpose of this PR is to describe my implementation of parallelism inside Pirouette. It is not fully working, and is based on the niols/just-be-bourrin branch which implements checking for satisfiability at every node instead of every leaf of the symbolic execution tree. I'll comment my change in subsequent messages.