[ATVA2026] ARTIFACT - Parallel analysiS framework for Termination and non-Termination of Lasso programs

This artifact accompanies the paper "PaSTTeL: Parallel analysiS framework for Termination and non-Termination of Lasso programs". PaSTTeL is a C++17 tool implementing a modular parallel portfolio framework for termination and non-termination analysis of lasso programs, using SMT solvers Z3 4.15.4 and CVC5 1.3.3. The artifact allows reviewers to: - Build and run PaSTTeL on lasso trace instances in JSON format.- Run Ultimate Buchi Automizer (ULR-Baseline) on C and BPL programs to extract lasso traces.- Reproduce the experimental comparison between P-ULR (PaSTTeL instantiated à la Ultimate LassoRanker) and Ultimate LassoRanker (ULR-Baseline), including tables (Table.1), scatter plots (Fig. 6) and solver comparison (Fig. 7) from the paper. The artifact is packaged as a self-contained Docker image (Ubuntu 24.04, offline build). It includes the PaSTTeL C++ source, pre-compiled Ultimate Buchi Automizer, pre-packaged solver archives (Z3, CVC5), the full ATVA 2026 benchmark (1,852 C programs, 862 BPL programs), pre-computed results from the paper, and evaluation scripts covering a quick smoke test (~2–5 minutes) and the full benchmark pipeline.