These are the measurement scripts for the HSCC 2019 paper "Numerical Verification of Affine Systems with up to a Billion Dimensions".

Each folder contains a python 2.7 script (run*.py) that can be run to perform the measurements or make the plots used in the paper. For some benchmarks there are gnuplot .plot files that can produce the images from the data output by the run script.

You need the continuous branch of the Hylaa tool installed. The exact verision used for these benchmarks can be downloaded here: https://github.com/stanleybak/hylaa/releases/tag/continuous-Dec18

Note: for the high-dimensional benchmarks you'll need a system with a large main memory. We used Amazon Web Services Elastic Computing Cloud (EC2) to rent a powerful m4.10xlarge instance with 40 cores and 160 GB of memory.

For the replicated helicopter benchmark, you'll also need Hyst (and hypy) installed and working with SpaceEx. The download and instructions for this are in the Hyst repository: https://github.com/stanleybak/hyst . If you just want to directly run SpaceEx manually on some of the models, the xml and cfg files are in the "heli/plot/spaceex_models" folder.
Since this benchmark exhausts memory for the various methods, it's best to do one tool at a time. This can be done by editing line 48 of make_plot_data.py to one of: 'spaceex', 'hylaa', 'rk45', 'krylov'.



Prepared by Stanley Bak, Dec 2018
