Submission
Competition contributions consist of the following parts:
- (i) an Easychair registration record at the SV-COMP submission site to register a tool for participation, the record must have a title that starts with the tool name, all team members as authors, and a short abstract, the last line of the abstract should specify who serves as jury member, no PDF required,
- (ii) an executable tool (= competition candidate) to be published at Zenodo, which serves as our verifier repository,
- (iii) a tool-info module for BenchExec (to be added to the BenchExec repository), the name of which should be mentioned in the registration record (i),
- (iv) a benchmark definition (to be added to the competition repository), the name of which should be mentioned in the registration record (i), and
- (v) a tool entry at the FM-Tools repository, with a version entry (DOI of the archive in (ii)) and a participation declaration, to be created via a merge request,
- (vi) optionally, 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, selected system descriptions will be published in the TACAS proceedings, the papers to be published must have 4 pages of text (excl. data-availability and funding statements, references) in LNCS style.
In order to participate, two actions are required by the deadline:
- (i): Register your tool for participation (first tool deadline).
- (ii) – (v): Required for pre-runs (second tool deadline).
Requirements for (i) System Description
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. It is a good idea to mention the name of the tool and/or technique (or a combination thereof) in the title. Please mark the jury member in the paper (asterisk after the name and footnote, perhaps). -
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 not replicable)
- Installation instructions
- 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
-
6. Data-Availability Statement
Publish (e.g., on Zenodo) your tool archive and reference it here (via DOI) to ensure reproducibility, also provide the URL of the project web site and repository. References
Bibliographic references to more in-depth papers about the approaches used in the tool.
Requirements for (ii) Executable Tool, (iii) Tool-Info Module, and (iv) Benchmark Definition
See rules under "Competition Environment and Requirements" and "Qualification".