Learning Symbolic Invariants
In this site you can find the tool and experiments that are part of the paper Learning to Prune Infeasible Paths in Generalized Symbolic Execution submitted to ISSRE 2022.
Getting started
Download the tool
Prerequisites
Make sure that you have installed the following tools:
Java 7
Python3
Installation
Uncompress the downloaded file in your working directory, open Eclipse and import all the existent projects from your working directory by selecting File, then Import, then General and then Existing Projects into Workspace. When finished, you should have the following projects:
jpf-core
jpf-symbc
jpf-symbc-bounded
Experiments
The experiments we performed are detailed in the following pages:
A single case study explains all the steps that you need to perform in order to reproduce the experiments regarding the symbolic execution times for the AvlTree case study
Training neural networks contains the details on training and evaluating the neural networks
Symbolic execution times shows the Symbolic Execution times of our technique compared with Lazy Initialization
Test suites quality shows the how to reproduce the experiment performed to analyze the quality of the test suites produced with our technique and with Lazy Initialization