Symnet

Symbolic execution for verification of stateful data planes made easy and fast.

Setup (*nix machine)

1. JDK 8 (in case a different one is used the ScalaZ3 jar needs to be rebuilt against this, different, JDK)
2. sbt - The simple build tool for Scala projects

See setup.sh for a concrete setup script (it was tested on 64bit Ubuntu 12.04, 14.04 and 15.10).

Then from project root issue sbt sample.

Setup (Vagrant)

There is also a Vagrantfile if you prefer this option. This also uses setup.sh for provisioning.

If you choose to use setup.sh (or Vagrantfile + setup.sh) you should only grab those files since this includes the cloning of the repo.

Setup (Docker)

There is a Dockerfile if you prefer Docker over Vagrant. The Dockerfile has no dependency to the setup.sh.

If you want to use Docker to build/use symnet run the following commands:

docker build -t johscheuer/symnet .
docker run -ti johscheuer/symnet

# Run example
sbt sample

SEFL sample

See src/main/scala/change/v2/runners/experiments/SEFLRunner.scala to start experimenting with SEFL. sbt sample will run that code.

Click models in Symnet

Look at the description of the instructions method in src/main/scala/org/change/v2/Template.scala; try to understand what the instructions attatched to input port 0 do. Check src/main/resources/click_test_files/Template.click in order to get the complete picture.

From the project root issue sbt click which performs the symbolic execution of Template.click file.

You should find the output in template.output.

Play with the code, check the output. Loop.