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:

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