Parallel ReCal Supplementary material

Citation Author(s):
Giovanni
Denaro
Submitted by:
Giovanni Denaro
Last updated:
Thu, 11/07/2019 - 12:37
DOI:
10.21227/hwxc-cf61
Data Format:
License:
103 Views
Categories:
Keywords:
0
0 ratings - Please login to submit your rating.

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.

Instructions: 

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.