STLScope: artifact for "Diverse STL Counterexample Pools for Hybrid Automata: Generation and Selection" (SEFM 2026)

Zenodo (CERN European Organization for Nuclear Research)

Abstract

Artefact for the SEFM 2026 paper "Diverse STL Counterexample Pools for Hybrid Automata: Generation and Selection". Start with sefm26-paper-ae.pdf. Appendix A of the paper is the artefact evaluation appendix: the badge claims, the quick start and how to check each functional and reusability outcome. Everything else in this deposit is what it refers to. The artefact contains both stages of the paper. Generation (CExplorer). An extension of the STLMC bounded model checker that, instead of stopping at the first counterexample, excludes a generalization of each counterexample it finds and continues the search, collecting a pool. It supports three generalization strategies: continuous, location-sequence, and symbolic. Selection (STLScope). A tool that applies diversity metrics across a pool of counterexamples, considering location, trajectory, initial-condition axes, and their combinations, using selection algorithms like greedy max-min and k-medoids to provide a small, diverse subset for a tester to review. Contents sefm26-paper-ae.pdf. The paper, with the artefact evaluation instructions as Appendix A. stlscope-artifact.tar.gz. Docker image with everything built and configured: CExplorer, the SMT solvers (Z3, Yices 2, SMT-RAT), STLScope, the counterexample pools, and the reference outputs of the analysis reported in the paper. stlscope-source.tar.gz. The STLScope repository. stlscope-pools.tar.gz. The counterexample pools, as a separate archive. ARTIFACT.md. Quick-start guide, available to read here without downloading anything. checksums.txt. SHA-256 for every file above. Getting started docker load -i stlscope-artifact.tar.gz docker run --rm --platform linux/amd64 stlscope-artifact sanity mkdir -p out docker run --rm --platform linux/amd64 -v "$PWD/out:/out" \ stlscope-artifact reproduce reproduce recomputes the analysis using the included pools in about a minute and compares each result to the reference outputs. Regeneration with CExplorer is supported and controlled by editable declarative configurations. ARTIFACT.md documents the full command surface. Section 3.2 of the paper refers to the artefact for a proof of the exactness of the trajectory distance. That proof is included in the image under doc/, and is copied to out/doc/ by any command that mounts an output directory. Licensed under GPL-3.0-only. Third-party components (STLMC, Yices 2, Z3, SMT-RAT) are documented in THIRD_PARTY.md inside the artefact.

Authors 5

1. Sergio Quijano

   IT University of Copenhagen

   Affiliation as printed

   IT University of Copenhagen

2. Arapatsakos Georg Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University

3. Erika Abraham Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University

4. Mahsa Varshosaz

   IT University of Copenhagen

   Affiliation as printed

   IT University of Copenhagen

5. Andrzej Wąsowski

   IT University of Copenhagen

   Affiliation as printed

   IT University of Copenhagen