Validating Code Changes Using Symbolic Execution

Notes

Report

• Java 8
• Z3

• ant clean
• ant bootstrap
• ant resolve
• ant build

To run any of the examples (or another project on a separate directory in the examples directory) you could use the shell script provided:

# Apply patches and generate Symbv tests
./bin/symbv example_name gen

# Compile everything
ant build

# Concolic/Symbolic execution
./bin/symbv example_name symbv

The last command could be replaced by two other options (for prune optimization or full symbolic execution):

# Prune Optimization
./bin/symbv example_name prune

# Symbolic execution
./bin/symbv example_name symbolic

• Run ant bootstrap - boostraps ivy install
• Run ant resolve - downloads the dependencies and places them in the lib directory
• Run ant build - builds the project
• Run ant test - runs test cases

1. Add dependency to ivy.xml
2. Run ant resolve
3. Add new jars to .classpath under the 3rd party jars section (this could be useful: cd lib; for f in *.jar; do echo "<classpathentry kind=\"lib\" path=\"lib/$f\"/>"; done)