PARQ is an automatic parallelization engine based on Skolem Function Synthesis and Quantified Invariant Generation. It is aimed at parallelization of array modifying programs written as Constrained Horn Clause (CHC) formulas.
parallel-computing distributed-computing verification locality invariants automatic-parallelization chc smt-solving
-
Updated
Nov 14, 2021 - SMT