What does this research mean for the field?

PaSTTeL provides a modular parallel portfolio framework for the termination and non-termination analysis of lasso programs, enabling reproducible performance comparisons against existing baselines like Ultimate LassoRanker. Novelty: ClaimNovelty.METHODOLOGICAL. Consensus alignment: ConsensusAlignment.NEUTRAL.

What question did this study set out to answer?

To present a robust framework for assessing termination and non-termination of lasso programs using a modular approach.

May 31, 20260 citationsOpen Access

View Full Paper

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

AKAnissa KheireddineSorbonne Université

Key Points

To present a robust framework for assessing termination and non-termination of lasso programs using a modular approach.
Developed PaSTTeL tool using C++17 for parallel termination analysis.
Utilized SMT solvers Z3 4.15.4 and CVC5 1.3.3 for program analysis.
Provided a Docker image containing all necessary components for running the framework.
Facilitated reproduction of experimental comparisons between P-ULR and Ultimate LassoRanker.
Included comprehensive benchmarks with 1,852 C programs and 862 BPL programs.
Delivered pre-computed results and evaluation scripts to streamline analysis processes.

Abstract

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.

Perguntar à IA

Bookmark

View Full Paper

Cite This Study

Anissa Kheireddine (Fri,) studied this question.

synapsesocial.com/papers/6a1bd1db5783ba022b6fd48e https://doi.org/https://doi.org/10.5281/zenodo.20437322

Perguntar à IA

Bookmark

View Full Paper