Reproduction Package for TACAS 2022 Article `CoVeriTeam: On-Demand Composition of Cooperative Verification Systems'

This file describes the contents of the replication package for the article “CoVeriTeam: On-Demand Composition of Cooperative Verification Systems”, submitted to TACAS 2022. This artifact has been created for evaluation using TACAS’22 Artifact Evaluation Virtual Machine for VirtualBox available via Zenodo (https://doi.org/10.5281/zenodo.5537146). Authors Dirk Beyer and Sudeep Kanav LMU Munich, Germany License SPDX-License-Identifier: CC-BY-4.0 https://spdx.org/licenses/CC-BY-4.0.html Some parts of this archive are licensed differently. For details see LICENSE.txt. Contents of this archive LICENSE.txt : specifies the license README.txt : this file coveriteam/ : folder containing necessary files to execute the examples in the submitted paper. It has been created from the repository: https://gitlab.com/sosy-lab/software/coveriteam packages/ : directory containing the packages that need to be installed to successfully run the examples downgrade-libc6/ : directory containing the deb packages required to downgrade libc6 (it is required to install gcc-multilib, which is required to execute the examples) configure_cgroups.sh: script to configure cgroups which are necessary for execution of a tool in a container. The remaining part of this README is structured as follows: first we provide instructions to setup the TACAS’22 virtual machine for artifact evaluation, then we describe execution of a single example CoVeriTeam program, then we give instructions for executing all the examples in the paper, and at last we point the interested reviewer to the documentation for using CoVeriTeam in general. Setup the TACAS’22 virtual machine to run the examples in the artifact This section describes the steps needed to setup the TACAS’22 virtual machine to execute CoVeriTeam on the examples provided in this artifact. Start the virtual machine, and login using the provided credentials. Copy the provided artifact archive (named CoVeriTeam-artifact-TACAS22-submission.zip) to the home directory of the virtual machine, and unzip it there. It should create a directory named CoVeriTeam-artifact-TACAS22-submission in the home directory. NOTE: PLEASE COPY. The tool WILL NOT EXECUTE from the mounted device. go to the directory “~/CoVeriTeam-artifact-TACAS22-submission” cd ~/CoVeriTeam-artifact-TACAS22-submission downgrade-libc6: we need to downgrade libc6 in order to install gcc-multilib. Please execute the following command. cd downgrade-libc6 sudo dpkg -i *.deb sudo apt --assume-yes --fix-broken install sudo apt --assume-yes autoremove cd .. install required packages by running the following commands cd packages sudo dpkg -i *.deb cd .. Configure cgroups: execute the script cgroups_setup.sh to configure cgroup for container execution and measurements ./configure_cgroups.sh Note: you will need to run the script “configure_cgroups.sh” each time the VM is rebooted the above script generally suffices to set the cgroups and the user should be able to execute the below command. If not, then the below command will print a command that needs to be executed to complete the cgroups setup. Executing a single example go to the directory “coveriteam/examples” execute the following command: ../bin/coveriteam verifier.cvt \ --input verifier_path=../actors/cpa-seq.yml \ --input verifier_version=default \ --input program_path=c/Problem02_label16.c \ --input specification_path=properties/unreach-call.prp \ --data-model ILP32 On successful execution CoVeriTeam creates a folder with a unique ID in the folder called “cvt-output”, and a link named “lastexecution” pointing to it. This folder contains: an xml named execution_trace.xml containing the execution trace of the the CoVeriTeam program. This trace contains resources consumed by executions of atomic actors, paths to artifacts produced and consumed during execution. folders containing artifacts for each execution, e.g., log file, witnesses, test suite, etc. Executing all the examples in the paper go to the directory coveriteam/examples execute examples_in_paper.sh - this file lists the commands for different CoVeriTeam examples in a sequence. Executing it will execute all the examples. You can also take individual commands from this file and execute is separately. Executing CoVeriTeam in general The file coveriteam/README.md provides more information about how to execute CoVeriTeam in general. The file coveriteam/doc/index.md provides more information about the input parameters of CoVeriTeam. A user can also get this information by executing bin/coveriteam --help The file coveriteam/examples/examples_in_paper.sh contains the commands which can be executed from the coveriteam folder to execute individual examples