Detailed analysis of dataset is available in an accompanying Jupyter Notebook in Google Colab.
- Build the verification jobs
docker build -t verify-mbedtls . --file docker/verify-mbedtls.Dockerfile
- Run benchmark and collect results
docker run -e SEAHORN_ROOT_REL=/home/usea/seahorn -it verify-mbedtls
In the docker container you will be in /home/usea/verify-mbedtls. From here, run the benchmark script.
bash scripts/run_benchmarks.sh
The results will be in five files. Copy these files to host for analysis.
'results_flight_append.json'
'results_write_records.json'
'results_write_handshake_shad.json'
'results_write_handshake_main.json'
'result_many_buffers.json'
The modified SEABMC sources can be found in this repo.