What is qCORAL?
qCORAL is a tool for the efficient quantification of solution spaces for arbitrarily complex constraints over bounded floating-point domains with inputs following non-uniform probabilistic distributions. qCORAL follows a layered compositional strategy, which splits up the estimation for a set of symbolic conditions (describing the program paths leading to the occurrence of the target event) into the estimation of individual symbolic conditions. Each symbolic condition is in turn decomposed into a set of independent clauses that can be analyzed separately and the estimated results are composed back together. This divide-and-conquer strategy speeds up the analysis by reducing large problems into sub-problems that are easier to analyze, and also allows the reuse of partial results for clauses appearing in several constraints.
For each independent clause, qCORAL further uses an off-the-shelf interval constraint solver to break the solution spaces into even smaller regions, whose union necessarily bounds the solution space of the clause. qCORAL then uses stratified sampling, a well known technique for speeding up the convergence of Monte Carlo simulations, to analyze the data from the independent regions and to compose the results. To speed-up the convergence rate of the analysis, qCORAL supports three strategies for iterative sampling allocation, which focus the sampling on the constraints that have the largest influence on the estimated results.
Use the top bar to navigate through our documentation.