/verification-group-project

An experiment on symbolic execution performance with static typing (Java - jpf) and dynamic typing (Python - PyExZ3)

Primary LanguageJava

#Symbolic Execution with Static and Dynamic Typing ##Software Verification and Validation Group Project, Spring 2015

Team Members:

  • Jon Beverly
  • Walter Scarborough
  • Aaron Wood

###Overview

This project was created as an experiment to test symbolic execution performance and path differences in Java and Python. We chose to test three sorting algorithms (bubble sort, quick sort and merge sort) in a range of input sizes using JPF (Java Pathfinder) and PyExZ3 (Z3 and CVC SMT solvers).

This repository contains code for our sorting algorithm implementations, symbolic execution wrappers, and instrumentation. It also contains data that we collected from running our experiments.