What is qCORAL?
qCORAL is a tool for the efficient quantification of solution spaces for arbitrarily complex constraints over bounded floating-point domains. 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.
How to Install?
- NOTE: If you want to reproduce our experiments, please follow the instructions available here.
Requirements
- RealPaver 0.4
- Download this file: realpaver-0.4.tar.gz
- Run "tar -xzvf realpaver-0.4.tar.gz" under the directory of your choice
- Make sure your environment satisfies the requirements listed under "HARDWARE AND SOFTWARE REQUIREMENTS" in README file
- Some dependencies are not listed in this file, like flex and bison.
- Run "./configure; make" (if 'configure' fails, try running only make)
- Java 1.7
Setup
- Download qCORAL here (source code)
- Uncompress the file somewhere
How to Interface with qCORAL?
From a Java program
qCORAL does not have a API yet, but you can invoke the analysis directly using the coral.counters.Main.runRegCoral(List<PC>, List<Interval[]>) method. For more details on how to call and configure qCORAL directly from Java, please see the source code. Send a email to mab@cin.ufpe.br if you have problems.
From the command-line
- Run "java -jar qcoral.jar $OPTIONS $INPUTFILE". Please see the list of command-line options, and the input language.
# run analysis without realpaver mateus@antenora:~/qcoral$ java -jar qcoral.jar --mcSkipPaving example_conflict #lots of output... [qCORAL] report for experiment example_conflict: [qCORAL] total time spent loading constraints (s): 0.286777 [qCORAL] total time spent running simulations (s): 10.215007 [qCORAL] result: 0.996560, error: NaN [qCORAL] tabulated data (order: estimate, stdev (if multiple executions were done), stdev (square of estimated variance), time, nsamples, file [qCORAL] full data: 0.9965599999999964 & NaN & 0.002244034243945488 & 10.501784 & 100000 & example_conflict [qCORAL-csvresults] file,estimate,stdev-multiple,stdev-varestimate,time,samples,n-exec [qCORAL-csvresults] example_conflict,0.996560,NaN,0.002244,10.501784,100000,1 #run analysis with realpaver mateus@antenora:~/qcoral$ java -jar qcoral.jar --realPaverLocation "/home/mateus/tools/realpaver-0.4/realpaver" example_conflict #.... [qCORAL] report for experiment example_conflict: [qCORAL] total time spent loading constraints (s): 0.181531 [qCORAL] total time spent running simulations (s): 13.715677 [qCORAL] result: 0.996500, error: NaN [qCORAL] tabulated data (order: estimate, stdev (if multiple executions were done), stdev (square of estimated variance), time, nsamples, file [qCORAL] full data: 0.9964999649996502 & NaN & 2.2745531223088825E-4 & 13.897208 & 100000 & example_conflict [qCORAL-csvresults] file,estimate,stdev-multiple,stdev-varestimate,time,samples,n-exec [qCORAL-csvresults] example_conflict,0.996500,NaN,0.000227,13.897208,100000,1 #run analysis with realpaver + partitioning + caching mateus@antenora:~/Dropbox/mestrado/qcoral$ java -jar qcoral.jar --realPaverLocation "/home/mateus/tools/realpaver-0.4/realpaver" --mcPartitionAndCache --mcCallIntSolPartition example_conflict #.... [qCORAL] report for experiment example_conflict: [qCORAL] total time spent loading constraints (s): 0.187308 [qCORAL] total time spent running simulations (s): 12.574735 [qCORAL] result: 0.996500, error: NaN [qCORAL] tabulated data (order: estimate, stdev (if multiple executions were done), stdev (square of estimated variance), time, nsamples, file [qCORAL] full data: 0.9964999649996502 & NaN & 2.2745531223088825E-4 & 12.762042 & 100000 & example_conflict [qCORAL-csvresults] file,estimate,stdev-multiple,stdev-varestimate,time,samples,n-exec [qCORAL-csvresults] example_conflict,0.996500,NaN,0.000227,12.762042,100000,1