Table des matières: :: Library Catalog

Enregistré dans:

Détails bibliographiques
Auteur principal:	Britikov, Konstantin
Format:	Recurso digital
Langue:	anglais
Publié:	Zenodo 2025
Accès en ligne:	https://doi.org/10.5281/zenodo.16919602
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Table des matières:

## CHC-Based Reachability Analysis via Cycle Summarization Artifact This README describes an artifact for iFM2025. It contains an information on how to reproduce and execute the evaluation of the artifact. It is structured as follows: - `README.md` - instructions file you're currently reading - `LICENSE` - license file of the artifact - `licenses` - directory containing licenses of the tools used in the artifact (Eldarica, Loat, Z3). - `ifm25arifact.ova` - Ubuntu 22.04 virtual machine that allows to reproduce the experementation. It can be executed with [VirtualBox](https://www.oracle.com/virtualization/technologies/vm/downloads/virtualbox-downloads.html).  Experiments were executed on the machine with 8 processors and 16 GB of RAM. ### Availability Artifact can be accessed with the following link: To access the virtual machine you should log with following credentials: - Username: `ifm25` - Password: `ifm25` ## Smoke Test To reproduce the experiments we recommend first to execute Smoke tests on the virtual machine (takes up to 15 minutes).  To do it follow the next steps: 1. Open Terminal application in the left top corner. 2. Type in the terminal following command: ```bash cd ~/Documents ``` 3. Execute Smoke Test by executing the following command: ```bash ./run_smoke_test.sh ``` After the execution it should produce 5 different png images of plots in the `~/Documents` folder.  If it is the case, it means that smoke tests were succesfully executed. ## Functionality Next step is to run the overall evaluation (can take up to 8 hours) 1. With Terminal open within `~/Documents` directory execute the evaluation: ```bash ./run_smoke_test.sh ``` After the execution it will produce 5 png images of plots in the `~/Documents` folder which compare the execution time of CSRA with different tools and engines that corresppond to the plots in Fig.2 and Fig.3 of the paper. To obtain more detailed information about the run you can access `~/Documents/artifact_files/experiments`, where `nested_<tool>.plot` contains the detailed information about execution time of CSRA compared to a specific tool.  Directories `eldarica`, `z3_spacer`, `loat_abmc`, `golem_<engine>` contain execution logs for every single benchmark. ## Reusability Artifact contains the full source code of the implementation and binary executable of the Golem with implemented CSRA approach. It can be found in the `~/Documents/artifact_files/solvers/golem` directory. To reproduce the execution outside of the virtual machine (or use tool on its own) it is possible to download and install golem from the [GitHub](github.com/usi-verification-and-security/golem). Specifically, the `nested-loops` branch should be used. Golem requires `CMake`, `gmp`, `bison` and `flex` to be installed, which can be installed using the following command: ```bash apt install -y apt-utils make cmake build-essential libgmp-dev libedit-dev bison flex  ``` And compiled using following set of commands from the golem root directory: ```bash git checkout nested-loops mkdir build cd build cmake .. make -j4 ``` Afterwards CSRA can be executed by calling ```bash ./golem --engine split-tpa <file> ``` Experiments are also available via [GitHub](https://github.com/BritikovKI/nested-benchmarks). Tool can be used for  reachability analysis of any LIA-lin, LRA-lin CHC problems (encoded in .smt2 format).

Documents similaires