Submission
Competition Contributions consist of three parts:
- (i) a system description that describes the competition contribution, including an outline of the concepts, technology, libraries, and tool infrastructure used in the competition, installation instructions, a specification of the version and parameters to be used for the competition,
- (ii) a link to the executable tool (= competition candidate), which should be mentioned in the system description, and
- (iii) a tool-info module for BenchExec (to be added to the BenchExec repository), the name of which should be mentioned in the system description.
Requirements for (i) System Description
Submit your system description via the SV-COMP'16 submission site of Easychair. System descriptions have a maximum of 3 pages in LNCS style.
The competition contribution paper should be structured as follows (the structure is recommended, not mandatory; but the below-mentioned information must be provided):
-
Title, Authors, and Abstract
The format is defined in the usual LNCS style. In addition, one author has to be indicated as corresponding author (in case clarification is necessary). It is a good idea to mention the name of the tool and/or technique (or a combination thereof) in the title. -
1. Verification Approach
A short overview of the theory that the tool is based on. Description of the abstract domains and algorithms that are used. Reference to the concept papers that describe the technical details. -
2. Software Architecture
- Libraries and external tools that the verification tool uses (e.g., parser frontend, SAT solver)
- Software structure and architecture (e.g., components that are used in the competition)
- Implementation technology (e.g., programming language)
-
3. Discussion of Strengths and Weaknesses of the Approach
Evaluation of the results for the benchmark categories, where was the checker successful, where not, why? -
4. Tool Setup and Configuration
- Download instructions (a public web page from which the tool can be downloaded) including a reference to a precise version of the tool (do not refer to ``the latest version'' or such, because that is not stable and reproducible)
- Installation instructions (including references to external public components that need to be installed, the dedicated competition machine runs Ubuntu 14.04 with an x86_64 GNU/Linux kernel and standard development packages, anything beyond that must be provided)
- Participation statement (a clear statement which categories the verifier participates in; consult the rules about opt-out statements)
- Configuration definition (there is one global set of parameters for all categories of the benchmark set, a full definition of the parameter set must be provided); check the rules page under Parameters for more details
-
5. Software Project and Contributors
- Contact info (web page of the project, people involved in the project)
- Information about the software project, licensing, development model, institution that hosts the software project, acknowledgement of contributors
References
Bibliographic references to more in depth papers about the approaches used in the tool.
Requirements for (ii) Executable Tool
See rules under "Setup" and "Qualification". The submitted system has to meet the following requirements:
- The verifier is publicly available for download.
- The verifier is archived in a .zip or .tgz file, the archive contains one single folder whose name starts with the verifier's name or acronym.
- The archive name starts with the verifier's name or acronym.
- The archive of the verifier contains a file LICENSE.txt that declares that the verifier can be used for the competition and for reproducing the results later.
- The archive does not contain repository data (.svn) and test files (and other unnecessary material).
- The verifier should not require any special software on the competition machines; all necessary libraries and external tools should be contained in the archive. Standard packages that are available as Ubuntu packages can be requested.
Requirements for (i) Tool-Info Module
In order to participate at SV-COMP, a tool-info module in the BenchExec repository is necessary. Technically, the tool-info module needs to be integrated into the BenchExec repository under directory benchexec/tools using a pull request.
The task of the tool-info module is (besides other tasks) to translate the output of a verifier to the results FALSE, TRUE, etc. For running the contributed verifier, the organizer follows the installation requirements and executes the verifier, relying on the tool-info module for correct execution of the verifier and correct interpretation of its results.