Datasets
Standard Dataset
Parallel ReCal Supplementary material
- Citation Author(s):
- Submitted by:
- Giovanni Denaro
- Last updated:
- Thu, 11/07/2019 - 12:37
- DOI:
- 10.21227/hwxc-cf61
- Data Format:
- License:
- Categories:
- Keywords:
Abstract
PURPOSE
-------
This data package is provided as supplementary material of the paper:
“A GPU Approach to Efficiently Reusing Constraint Proofs”, by M. Chen, G. Denaro and M. Pezzè,
submitted for evaluation to IEEE Transactions on software engineering, Nov. 2019.
STRUCTURE
---------
The data package consists of 24 files:
- a file named _README.txt: this file
- a file named _programs.txt
- 22 files named <program_name>.sexpr
File _programs.txt lists subject programs used in the experiments discussed in the paper. For each subject program, the file indicates an online reference where the code of the program can be found.
Each file named <program_name>.sexpr reports the QFLIA constraints that we considered for each subject program. Specifically, in each experiment, we executed a subject program with symbolic execution, and monitored the constraints (the ones in the file) sent to the constraint solver during the analysis of that program.
PURPOSE
-------
This data package is provided as supplementary material of the paper:
“A GPU Approach to Efficiently Reusing Constraint Proofs”, by M. Chen, G. Denaro and M. Pezzè,
submitted for evaluation to IEEE Transactions on software engineering, Nov. 2019.
STRUCTURE
---------
The data package consists of 24 files:
- a file named _README.txt: this file
- a file named _programs.txt
- 22 files named <program_name>.sexpr
File _programs.txt lists subject programs used in the experiments discussed in the paper. For each subject program, the file indicates an online reference where the code of the program can be found.
Each file named <program_name>.sexpr reports the QFLIA constraints that we considered for each subject program. Specifically, in each experiment, we executed a subject program with symbolic execution, and monitored the constraints (the ones in the file) sent to the constraint solver during the analysis of that program.